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:
011: package de.uka.ilkd.key.gui.prooftree;
012:
013: /** this class implements a TreeModel that can be displayed using the
014: * JTree class framework
015: */
016: import javax.swing.tree.TreeNode;
017:
018: import de.uka.ilkd.key.proof.ConstraintTableModel;
019: import de.uka.ilkd.key.proof.Node;
020:
021: class GUIBranchNode extends GUIAbstractTreeNode implements TreeNode {
022:
023: private Node subTree;
024: private Object label;
025:
026: public GUIBranchNode(GUIProofTreeModel tree, Node subTree,
027: Object label) {
028: super (tree);
029: this .subTree = subTree;
030: this .label = label;
031: }
032:
033: private TreeNode[] childrenCache = null;
034:
035: private void createChildrenCache() {
036: childrenCache = new TreeNode[getChildCountHelp()];
037: }
038:
039: public TreeNode getChildAt(int childIndex) {
040: fillChildrenCache();
041: return childrenCache[childIndex];
042:
043: /*
044: int count = 0;
045: Node n = subTree;
046: while ( childIndex != count
047: && n.childrenCount() == 1 ) {
048: count++;
049: n = n.child(0);
050: }
051: if ( childIndex == count ) {
052: return getProofTreeModel ().getProofTreeNode(n);
053: } else {
054: return findBranch ( n.child(childIndex-count-1) );
055: }
056: */
057: }
058:
059: private void fillChildrenCache() {
060: if (childrenCache == null)
061: createChildrenCache();
062: if (childrenCache.length == 0 || childrenCache[0] != null)
063: return;
064:
065: int count = 0;
066: Node n = subTree;
067: while (true) {
068: childrenCache[count] = getProofTreeModel()
069: .getProofTreeNode(n);
070: count++;
071: final Node nextN = findChild(n);
072: if (nextN == null)
073: break;
074: n = nextN;
075: }
076:
077: final ConstraintTableModel userConstraint = n.proof()
078: .getUserConstraint();
079:
080: for (int i = 0; i != n.childrenCount(); ++i) {
081: if (!getProofTreeModel().hideClosedSubtrees()
082: || !userConstraint.displayClosed(n.child(i))) {
083: childrenCache[count] = findBranch(n.child(i));
084: count++;
085: }
086: }
087: }
088:
089: public void flushCache() {
090: childrenCache = null;
091: }
092:
093: public int getChildCount() {
094: if (childrenCache == null)
095: createChildrenCache();
096: return childrenCache.length;
097: }
098:
099: private int getChildCountHelp() {
100: int count = 0;
101: Node n = subTree;
102: while (true) {
103: count++;
104: final Node nextN = findChild(n);
105: if (nextN == null)
106: break;
107: n = nextN;
108: }
109: final ConstraintTableModel userConstraint = n.proof()
110: .getUserConstraint();
111: for (int i = 0; i != n.childrenCount(); ++i) {
112: if (!getProofTreeModel().hideClosedSubtrees()
113: || !userConstraint.displayClosed(n.child(i))) {
114: count++;
115: }
116: }
117: return count;
118: }
119:
120: public TreeNode getParent() {
121: Node n = subTree.parent();
122: if (n == null) {
123: return null;
124: } else {
125: while (n.parent() != null && findChild(n.parent()) != null) {
126: n = n.parent();
127: }
128: return findBranch(n);
129: }
130: }
131:
132: public Node getNode() {
133: return subTree;
134: }
135:
136: // signalled by GUIProofTreeModel when the user has altered the value
137: public void setLabel(String s) {
138: subTree.getNodeInfo().setBranchLabel(s);
139: }
140:
141: public boolean isLeaf() {
142: return false;
143: }
144:
145: public String toString() {
146: String res = subTree.getNodeInfo().getBranchLabel();
147: if (res == null)
148: return label.toString();
149: return res;
150: }
151:
152: }
|