package gve.calc.logic;

import java.awt.*;
import gve.calc.formula.*;
import gve.calc.formula.Part;

public class ProofRuleView extends TabularView {
	public ProofRuleView(ProofRule model,FormulaView view) {
		super(model,view);
		TabularLayout layout = (TabularLayout)getLayout();
		layout.setHgap(2);
	}

	public void paint(Graphics g) {
		super.paint(g);
		Dimension siz = getSize();
		FormulaView view = FormulaView.get(this);
		ProofRule model = (ProofRule)getModel();
		// Rules beside name
		int y = 0;
		{	Component nam = view.getView(model.rules[0]);
			if (nam instanceof HasBaseline)
				y = ((HasBaseline)nam).getBaseline()/2;
			int w = nam.getSize().width;
			g.drawLine(0,y,(siz.width-w)/2-2,y);
			g.drawLine(siz.width,y,(siz.width+w)/2+1,y);
		}	
		// Border around formula
		g.drawLine(0,y,0,siz.height-1);
		g.drawLine(0,siz.height-1,siz.width-1,siz.height-1);
		g.drawLine(siz.width-1,siz.height-1,siz.width-1,y);
		// Rule between conditions and conclusion
		y = siz.height - view.getView(model.rules[model.getHeight()-1]).getSize().height - TabularLayout.VSPACE/2 - 2;
		g.drawLine(3,y,siz.width-3,y);
	}

	public boolean keydn(int key) {
		FormulaView view = FormulaView.get(this);
		ProofRule model = (ProofRule)getModel();
		if (key == Key_BS) {
			Point p = model.whichOffspring(view.getCursorPart());
			if (p == null) return super.keydn(key);
			if (p.y>0 && Part.isEmpty(model.rules[p.y])) {
				model.removeRow(p.y);
				view.setCursorPart(model.rules[p.y-1]);
				return true;
			}
		}
		if (key != '\n') return super.keydn(key);
		int child;
		{	Point p = model.whichOffspring(view.getCursorPart());
			if (p == null) return super.keydn(key);
			child = p.y;
		}
		if (child == model.rules.length) return super.keydn(key);
		model.insertRow(child+1);
		view.setCursorPart(model.rules[child+1]);
		return true;	
	}
}