package gve.calc.logic;

import awt.*;
import java.awt.*;
import awt.Button;
import java.awt.event.*;
import gve.calc.formula.*;
import gve.calc.logic.*;

public class OperatorModelView extends InfixBinaryOpView implements ActionListener,CreatesPopup {
	public OperatorModelView(OperatorModel model,FormulaView view,Component operatorView) {
		super(model,view,operatorView);
	}

	public Component createPopup(int x,int y) {
		awt.Button b;
		OperatorModel model = (OperatorModel)getModel();
		Container cont = new Panel();
		cont.setLayout(new GridPackLayout(0,1));
		cont.add(b = new Button("Swap operands"));
		b.addActionListener(this);
		if (model.getKind() == OperatorModel.TRIANGLE) {
			cont.add(b = new Button("Add branch"));
			b.addActionListener(this);
		} else if (model.getKind() == OperatorModel.ASSERTION) {
			{	// Don't add a 'start proof' menu if we are already inside a proof.
				Part p;
				for (p = model.getParent(); p != null; p = p.getParent()) {
					if (p instanceof Proof) break;
				}
				if (p == null) {
					cont.add(b = new Button("Start proof"));
					b.addActionListener(this);
				}
			}
			cont.add(b = new Button("New proof rule"));
			b.addActionListener(this);
		}
		return cont;
	}

	public void actionPerformed(ActionEvent evt) {
		String cmd = evt.getActionCommand();
		FormulaView view = FormulaView.get(this);
		Formula f = view.getFormula();
		OperatorModel model = (OperatorModel)getModel();
		if (cmd.equals("Add branch")) {
			Part dummy = new Identifier("");
			Identifier child;
			f.replace(model,new TableauPart(dummy,child = new Identifier("")));
			f.replace(dummy,model);
			view.setCursorPart(child);
		} else if (cmd.equals("Start proof")) {
			Part dummy = new Identifier("");
			f.replace(model,dummy);
			f.replace(dummy,new Proof(model));
			view.setCursorPart(model);
		} else if (cmd.equals("New proof rule")) {
			Part dummy = new Identifier("");
			f.replace(model,dummy);
			ProofRule rule;
			f.replace(dummy,rule = new ProofRule(model));
			view.setCursorPart(rule.elementAt(0,0));
		} else super.actionPerformed(evt);
	}
}