001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010: package de.uka.ilkd.key.gui.prooftree;
011:
012: import java.util.Enumeration;
013: import java.util.LinkedList;
014:
015: import javax.swing.tree.TreeNode;
016:
017: import de.uka.ilkd.key.proof.ConstraintTableModel;
018: import de.uka.ilkd.key.proof.Node;
019:
020: public abstract class GUIAbstractTreeNode implements TreeNode {
021:
022: private GUIProofTreeModel tree;
023:
024: protected GUIProofTreeModel getProofTreeModel() {
025: return tree;
026: }
027:
028: public GUIAbstractTreeNode(GUIProofTreeModel tree) {
029: this .tree = tree;
030: }
031:
032: public abstract TreeNode getChildAt(int childIndex);
033:
034: public abstract int getChildCount();
035:
036: public abstract TreeNode getParent();
037:
038: public abstract boolean isLeaf();
039:
040: public int getIndex(TreeNode node) {
041: for (int i = 0; i < getChildCount(); i++) {
042: if (getChildAt(i).equals(node)) {
043: return i;
044: }
045: }
046: return -1;
047: }
048:
049: public boolean getAllowsChildren() {
050: return !isLeaf();
051: }
052:
053: public Enumeration children() {
054: return new ChildEnumeration();
055: }
056:
057: public Object[] getPath() {
058: LinkedList path = new LinkedList();
059: TreeNode n = this ;
060: // System.out.println("1: "+n);
061: path.addFirst(n);
062: while ((n = n.getParent()) != null) {
063: // System.out.println("2: "+n+ " "+path);
064: path.addFirst(n);
065: }
066: return path.toArray();
067: }
068:
069: protected TreeNode findBranch(Node p_node) {
070: TreeNode res = getProofTreeModel().findBranch(p_node);
071: if (res != null)
072: return res;
073:
074: String label = p_node.getNodeInfo().getBranchLabel();
075:
076: if (p_node.root()) {
077: label = "Proof Tree";
078: }
079: if (label == null) {
080: label = "Case " + (p_node.parent().getChildNr(p_node) + 1);
081: p_node.getNodeInfo().setBranchLabel(label);
082: }
083:
084: return getProofTreeModel().getBranchNode(p_node, label);
085: }
086:
087: private class ChildEnumeration implements Enumeration {
088: int current = 0;
089:
090: public boolean hasMoreElements() {
091: return current < getChildCount();
092: }
093:
094: public Object nextElement() {
095: return getChildAt(current++);
096: }
097:
098: }
099:
100: public abstract Node getNode();
101:
102: protected Node findChild(Node n) {
103: if (n.childrenCount() == 1)
104: return n.child(0);
105:
106: if (!getProofTreeModel().hideClosedSubtrees())
107: return null;
108:
109: final ConstraintTableModel userConstraint = n.proof()
110: .getUserConstraint();
111:
112: Node nextN = null;
113: for (int i = 0; i != n.childrenCount(); ++i) {
114: if (!userConstraint.displayClosed(n.child(i))) {
115: if (nextN != null)
116: return null;
117: nextN = n.child(i);
118: }
119: }
120:
121: return nextN;
122: }
123: }
|