Copyright (C) 2000, 2001, Geert Vernaeve. All Rights Reserved. 
package gve.calc.formula;

import awt.*;
import java.awt.*;
import awt.Button;
import java.awt.event.*;
import gve.calc.logic.TableauPart;
import gve.calc.logic.OperatorModel;

public class OperatorNotView extends PrefixUnaryOpView implements ActionListener,CreatesPopup {
	public OperatorNotView(OperatorNot model,FormulaView view,Component operatorView) {
		super(model,view,operatorView);
	}

	public Component createPopup(int x,int y) {
		Button b;
		// is this the main operator of a formula on the left/right of a |> operator?
		Part p = (Part)getModel();
		while (p.parent instanceof OperatorComma) p = p.parent;
		if (p.parent instanceof OperatorModel
			&& ((OperatorModel)p.parent).getKind()==OperatorModel.TRIANGLE
			&& !TableauPart.hasReduction(p.parent)) {
			b = new Button("Reduce in tableau");
			b.addActionListener(this);
			return b;
		}
		return null;
	}

	public void actionPerformed(ActionEvent evt) {
		String cmd = evt.getActionCommand();
		if (cmd.equals("Reduce in tableau")) {
			Formula formula = FormulaView.get(this).getFormula();
			OperatorNot operator = (OperatorNot)getModel();
			Part p = operator;
			while (p.parent instanceof OperatorComma) p = p.parent;
			if (p.parent instanceof OperatorModel && ((OperatorModel)p.parent).getKind()==OperatorModel.TRIANGLE) {
				OperatorModel mod = (OperatorModel)p.parent;
				Part leftmod = new Identifier(),rightmod = new Identifier();
				// Add branch
				{	Part dummy = new Identifier();
					OperatorModel newmod = new OperatorModel(OperatorModel.TRIANGLE,leftmod,rightmod);
					formula.replace(mod,new TableauPart(dummy,newmod));
					formula.replace(dummy,mod);
				}
				if (p == mod.right) {	// Reduceren van rechterkant naar linkerkant
					Part leftclone;
					formula.replace(leftmod,leftclone = (Part)mod.left.clone());
					formula.replace(rightmod,OperatorComma.copyListExcept(mod.right,operator));
					// Add to left hand side.
					OperatorComma.addToFrontOfList(formula,leftclone,(Part)operator.child.clone());
				} else if (p == mod.left) {	// operator staat links, vliegt naar rechts
					formula.replace(leftmod,OperatorComma.copyListExcept(mod.left,operator));
					Part rightclone;
					formula.replace(rightmod,rightclone = (Part)mod.right.clone());
					// Add to right hand side
					OperatorComma.addToFrontOfList(formula,rightclone,(Part)operator.child.clone());
				}
			}
		}
	}
}