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: import java.util.Collection;
014: import java.util.Collections;
015: import java.util.HashMap;
016: import java.util.Stack;
017:
018: import javax.swing.event.EventListenerList;
019: import javax.swing.event.TreeModelEvent;
020: import javax.swing.event.TreeModelListener;
021: import javax.swing.tree.TreeModel;
022: import javax.swing.tree.TreeNode;
023: import javax.swing.tree.TreePath;
024:
025: import de.uka.ilkd.key.gui.configuration.ProofSettings;
026: import de.uka.ilkd.key.proof.*;
027: import de.uka.ilkd.key.util.Debug;
028:
029: /** An implementation of TreeModel that can be displayed using the
030: * JTree class framework and reflects the state of a
031: * {@link de.uka.ilkd.key.proof.Proof} object.
032: *
033: * <p>The tree structure of the proof is transformed, so that nodes
034: * following each other on a long branch are represented as kin, while
035: * new sutrees are displayed for branching points.
036: *
037: * <p>There are thus two kinds of node in this TreeModel,
038: * {@link de.uka.ilkd.key.gui.prooftree.GUIProofTreeNode}s, representing nodes of
039: * the displayed proof, and {@link de.uka.ilkd.key.gui.prooftree.GUIBranchNode}s
040: * representing branching points. (There is also one at the root.)
041: */
042:
043: class GUIProofTreeModel implements TreeModel, java.io.Serializable {
044:
045: private Proof proof;
046: private ProofTreeListener proofTreeListener;
047:
048: private EventListenerList listenerList = new EventListenerList();
049:
050: private boolean attentive = true;
051:
052: /** construct a GUIProofTreeModel that mirrors the given
053: * Proof.
054: */
055: public GUIProofTreeModel(Proof p) {
056: if (p == null) {
057: throw new IllegalArgumentException("null proof in "
058: + "GUIProofTreeModel().");
059: }
060: this .proof = p;
061: proofTreeListener = new ProofTreeListener();
062:
063: // proof.addProofTreeListener(proofTreeListener);
064: }
065:
066: class ProofTreeListener extends ProofTreeAdapter {
067:
068: public void proofStructureChanged(ProofTreeEvent e) {
069: Node n = e.getNode();
070: // we assume that there already is a "node" event for every other
071: // type of event
072: if (n != null) {
073: updateTree(getProofTreeNode(n));
074: return;
075: }
076:
077: Goal g = e.getGoal();
078: if (g != null) {
079: updateTree(getProofTreeNode(g.node()));
080: return;
081: }
082:
083: }
084:
085: public void proofGoalRemoved(ProofTreeEvent e) {
086: if (hideClosedSubtrees()) {
087: updateTree((TreeNode) null);
088: } else
089: proofStructureChanged(e);
090: }
091:
092: }
093:
094: /** Call this when the GUIProofTreeModel is no longer needed.
095: * GUIProofTreeModel registers a Listener with its associated
096: * Proof object. This method unregisters that listener, which is
097: * a good thing, as the proof maintains a reference to the
098: * listener, and the listener to the GUIProofTreeModel, so it would
099: * never become GC'ed unless you call this method.
100: *
101: * <p>Note that after calling <code>unregister</code>, this
102: * GUIProofTreeModel does not respond to changes in the proof tree
103: * any more.
104: */
105: public void unregister() {
106: proof.removeProofTreeListener(proofTreeListener);
107: }
108:
109: public void register() {
110: proof.addProofTreeListener(proofTreeListener);
111: }
112:
113: /** Sets whether this object should respond to changes in the
114: * the proof immediately. */
115: public void setAttentive(boolean b) {
116: Debug.out("setAttentive:", b);
117: if (b != attentive) {
118: if (b) {
119: proof.addProofTreeListener(proofTreeListener);
120: // updateTree(null);
121: if (hideClosedSubtrees()) {
122: updateTree((TreeNode) null);
123: }
124: } else {
125: proof.removeProofTreeListener(proofTreeListener);
126: }
127: attentive = b;
128: }
129: }
130:
131: /** returns true if the model respond to changes in the proof
132: * immediately */
133: public boolean isAttentive() {
134: return attentive;
135: }
136:
137: /**
138: * Adds a listener for the TreeModelEvent posted after the tree changes.
139: * Such events are generated whenever the underlying Proof changes.
140: *
141: * @see #removeTreeModelListener
142: * @param l the listener to add
143: */
144: public void addTreeModelListener(TreeModelListener l) {
145: listenerList.add(TreeModelListener.class, l);
146: }
147:
148: /**
149: * Removes a listener previously added with <B>addTreeModelListener()</B>.
150: *
151: * @see #addTreeModelListener
152: * @param l the listener to remove
153: */
154: public void removeTreeModelListener(TreeModelListener l) {
155: listenerList.remove(TreeModelListener.class, l);
156: }
157:
158: private boolean hideSubtrees = false;
159:
160: public boolean hideClosedSubtrees() {
161: return hideSubtrees;
162: }
163:
164: public void setHideClosedSubtrees(boolean hideSubtrees) {
165: if (this .hideSubtrees == hideSubtrees)
166: return;
167: this .hideSubtrees = hideSubtrees;
168: updateTree((TreeNode) null);
169: }
170:
171: public boolean isHidingIntermediateProofsteps() {
172: return ProofSettings.DEFAULT_SETTINGS.getViewSettings()
173: .getHideIntermediateProofsteps();
174: }
175:
176: /**
177: * Sets wether intermediate proofsteps should be shown or not and
178: * updates the tree.
179: */
180: public void hideIntermediateProofsteps(boolean hide) {
181: if (hide != isHidingIntermediateProofsteps()) {
182: ProofSettings.DEFAULT_SETTINGS.getViewSettings()
183: .setHideIntermediateProofsteps(hide);
184: updateTree((TreeNode) null);
185: }
186: }
187:
188: /**
189: * Decides wether a child should be counted while iterating all children.
190: * A child should not be counted if intermediate proofsteps are hidden and
191: * the child is not the last child, i.e. not an open or closed goal.
192: * Used by getChild, getChildCount and getIndexOfChild (implementing
193: * TreeModel).
194: */
195: private boolean countChild(TreeNode child, TreeNode parent) {
196: if (!isHidingIntermediateProofsteps()) {
197: return true;
198: }
199: if (child instanceof GUIProofTreeNode) {
200: int pos = -1;
201: for (int i = 0; i < parent.getChildCount(); i++) {
202: if (parent.getChildAt(i) == child) {
203: pos = i;
204: break;
205: }
206: }
207: if (pos == parent.getChildCount() - 1) {
208: return true;
209: }
210: // count if child is inlined by hide closed subtrees
211: if (hideClosedSubtrees()
212: && !(parent.getChildAt(pos + 1) instanceof GUIBranchNode)
213: && ((GUIProofTreeNode) child).getNode()
214: .childrenCount() != 1) {
215: return true;
216: }
217: return false;
218: } else if (child instanceof GUIBranchNode) {
219: return true;
220: }
221: return true;
222: }
223:
224: /**
225: * Returns the child of <I>parent</I> at index <I>index</I> in the parent's
226: * child array. <I>parent</I> must be a node previously obtained from
227: * this data source. This should not return null if <i>index</i>
228: * is a valid index for <i>parent</i> (that is <i>index</i> >= 0 &&
229: * <i>index</i> < getChildCount(<i>parent</i>)).
230: *
231: * @param parent a node in the tree, obtained from this data source
232: * @return the child of <I>parent</I> at index <I>index</I>
233: */
234: public Object getChild(Object parent, int index) {
235: if (isHidingIntermediateProofsteps()) {
236: TreeNode child;
237: int count = -1;
238: for (int i = 0; i < ((TreeNode) parent).getChildCount(); i++) {
239: child = ((TreeNode) parent).getChildAt(i);
240: if (countChild(child, (TreeNode) parent)) {
241: count++;
242: if (index == count) {
243: return child;
244: }
245: }
246: }
247: } else {
248: TreeNode guiParent = (TreeNode) parent;
249: if (guiParent.getChildCount() > index) {
250: return guiParent.getChildAt(index);
251: }
252: }
253: return null;
254: }
255:
256: /**
257: * Returns the number of children of <I>parent</I>. Returns 0 if the node
258: * is a leaf or if it has no children. <I>parent</I> must be a node
259: * previously obtained from this data source.
260: *
261: * @param parent a node in the tree, obtained from this data source
262: * @return the number of children of the node <I>parent</I>
263: */
264: public int getChildCount(Object parent) {
265: if (isHidingIntermediateProofsteps()) {
266: TreeNode child;
267: int count = 0;
268: for (int i = 0; i < ((TreeNode) parent).getChildCount(); i++) {
269: child = ((TreeNode) parent).getChildAt(i);
270: if (countChild(child, (TreeNode) parent)) {
271: count++;
272: }
273: }
274: return count;
275: } else {
276: return ((TreeNode) parent).getChildCount();
277: }
278: }
279:
280: /**
281: * Returns the index of child in parent.
282: *
283: * @param parent a node in the tree, obtained from this data source
284: * @param child a child of parent, obtained from this data source
285: * @return The index of child in parent
286:
287: */
288: public int getIndexOfChild(Object parent, Object child) {
289: TreeNode guiParent = (TreeNode) parent;
290: int count = -1;
291: if (isHidingIntermediateProofsteps()) {
292: for (int i = 0; i < guiParent.getChildCount(); i++) {
293: if (countChild(guiParent.getChildAt(i), guiParent)) {
294: count++;
295: if (guiParent.getChildAt(i) == child) {
296: return count;
297: }
298: }
299: }
300: } else {
301: for (int i = 0; i < guiParent.getChildCount(); i++) {
302: if (guiParent.getChildAt(i) == child) {
303: return i;
304: }
305: }
306: }
307: return -1;
308: }
309:
310: /**
311: * Returns the root of the tree. Returns null only if the tree has
312: * no nodes.
313: *
314: * @return the root of the tree
315: */
316: public Object getRoot() {
317: return getBranchNode(proof.root(), "Proof Tree");
318: }
319:
320: /**
321: * Returns true if <I>node</I> is a leaf. It is possible for this method
322: * to return false even if <I>node</I> has no children. A directory in a
323: * filesystem, for example, may contain no files; the node representing
324: * the directory is not a leaf, but it also has no children.
325: *
326: * @param guiNode a node in the tree, obtained from this data source
327: * @return true if <I>node</I> is a leaf
328: */
329: public boolean isLeaf(Object guiNode) {
330: return ((TreeNode) guiNode).isLeaf();
331: }
332:
333: /**
334: * Messaged when the user has altered the value for the item identified
335: * by <I>path</I> to <I>newValue</I>. We throw an exception,
336: * as proofs are not meant to be chaged via the JTree editing facility.
337: *
338: * @param path path to the node that the user has altered.
339: * @param newValue the new value from the TreeCellEditor.
340: */
341: public void valueForPathChanged(TreePath path, Object newValue) {
342: if (path.getLastPathComponent() instanceof GUIBranchNode) {
343: ((GUIBranchNode) path.getLastPathComponent())
344: .setLabel((String) newValue);
345: }
346: }
347:
348: /** Take the appropriate actions after a change in the Proof.
349: * Currently, this means throwing all cached Information away
350: * and fire an indiscriminating TreeStructureChanged event.
351: * This should probably be made more efficient.
352: */
353: private void updateTree(TreeNode trn) {
354: if (trn == null || trn == getRoot()) { // bigger change, redraw whole tree
355: proofTreeNodes = new HashMap();
356: branchNodes = new HashMap();
357: fireTreeStructureChanged(new Object[] { getRoot() });
358: return;
359: }
360: // otherwise redraw only a certain subtree
361: // starting from the parent of trn
362: flushCaches(trn);
363: Object[] path = ((GUIAbstractTreeNode) trn.getParent())
364: .getPath();
365: fireTreeStructureChanged(path);
366: }
367:
368: public void updateTree(Node p_node) {
369: if (p_node == null)
370: updateTree((TreeNode) null);
371: else
372: updateTree(getProofTreeNode(p_node));
373: }
374:
375: private void flushCaches(TreeNode trn) {
376: Node n = ((GUIAbstractTreeNode) trn).getNode();
377: while (true) {
378: final Node p = n.parent();
379: if (p == null
380: || ((GUIAbstractTreeNode) trn).findChild(p) == null)
381: break;
382: n = p;
383: }
384:
385: flushCaches(n);
386: }
387:
388: private void flushCaches(Node n) {
389: final Stack workingList = new Stack();
390: workingList.add(n);
391: while (!workingList.empty()) {
392: Node node = (Node) workingList.pop();
393: final GUIBranchNode treeNode = findBranch(node);
394: if (treeNode == null)
395: continue;
396: treeNode.flushCache();
397: while (true) {
398: final Node nextN = treeNode.findChild(node);
399: if (nextN == null)
400: break;
401: node = nextN;
402: }
403: final ConstraintTableModel userConstraint = node.proof()
404: .getUserConstraint();
405:
406: for (int i = 0; i != node.childrenCount(); ++i)
407: if (!treeNode.getProofTreeModel().hideClosedSubtrees()
408: || !userConstraint.displayClosed(node.child(i)))
409: workingList.add(node.child(i));
410: }
411: }
412:
413: /** Notify all listeners that have registered interest for
414: * notification on treeStructureChanged events.
415: */
416: protected void fireTreeStructureChanged(Object[] path) {
417: TreeModelEvent event = null;
418: // Guaranteed to return a non-null array
419: Object[] listeners = listenerList.getListenerList();
420: // Process the listeners last to first, notifying
421: // those that are interested in this event
422: for (int i = listeners.length - 2; i >= 0; i -= 2) {
423: if (listeners[i] == TreeModelListener.class) {
424: // Lazily create the event:
425: if (event == null)
426: event = new TreeModelEvent(this , path);
427: ((TreeModelListener) listeners[i + 1])
428: .treeStructureChanged(event);
429: }
430: }
431: }
432:
433: // caches for the GUIProofTreeNode and GUIBranchNode objects
434: // generated to represent the nodes resp. subtrees of the Proof.
435:
436: private HashMap proofTreeNodes = new HashMap();
437: private HashMap branchNodes = new HashMap();
438:
439: /** Return the GUIProofTreeNode corresponding to node n, if one
440: * has already been generated, and null otherwise.
441: */
442: public GUIProofTreeNode find(Node n) {
443: return (GUIProofTreeNode) (proofTreeNodes.get(n));
444: }
445:
446: /** Return the GUIProofTreeNode corresponding to node n.
447: * Generate one if necessary.
448: */
449: public GUIProofTreeNode getProofTreeNode(Node n) {
450: GUIProofTreeNode res = find(n);
451: if (res == null) {
452: res = new GUIProofTreeNode(this , n);
453: proofTreeNodes.put(n, res);
454: }
455: return res;
456: }
457:
458: /**
459: * Return the GUIBranchNode corresponding to the subtree rooted
460: * at n, if one has already been generated, and null otherwise.
461: */
462: public GUIBranchNode findBranch(Node n) {
463: return (GUIBranchNode) branchNodes.get(n);
464: }
465:
466: /**
467: * Return the GUIBranchNode corresponding to the subtree rooted
468: * at n. Generate one if necessary, using label as the the
469: * subtree label.
470: */
471: public GUIBranchNode getBranchNode(Node n, Object label) {
472: GUIBranchNode res = findBranch(n);
473: if (res == null) {
474: res = new GUIBranchNode(this , n, label);
475: branchNodes.put(n, res);
476: }
477: return res;
478: }
479:
480: Collection expansionState = Collections.EMPTY_SET;
481:
482: public void storeExpansionState(Collection c) {
483: expansionState = c;
484: //System.err.println("Proof "+proof.name()+" stor. state: "+ expansionState );
485: }
486:
487: public Collection getExpansionState() {
488: //System.err.println("Proof "+proof.name()+" retr. state: "+ expansionState );
489: return expansionState;
490: }
491:
492: TreePath selection;
493:
494: public void storeSelection(TreePath t) {
495: selection = t;
496: }
497:
498: public TreePath getSelection() {
499: return selection;
500: }
501:
502: }
|