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: /*
014: http://www.chka.de/swing/tree/expansion/ExpansionState.java
015: This code is provided by Christian Kaufhold <ch-kaufhold@gmx.de> under LGPL
016: */
017:
018: import java.beans.PropertyChangeEvent;
019: import java.beans.PropertyChangeListener;
020: import java.io.IOException;
021: import java.io.ObjectInputStream;
022: import java.io.Serializable;
023: import java.util.*;
024:
025: import javax.swing.JTree;
026: import javax.swing.event.TreeExpansionEvent;
027: import javax.swing.event.TreeExpansionListener;
028: import javax.swing.event.TreeModelEvent;
029: import javax.swing.event.TreeModelListener;
030: import javax.swing.tree.TreeModel;
031: import javax.swing.tree.TreePath;
032:
033: /** Cache/Access JTree's expansion state. The interface of JTree to access
034: the expanded paths is rather incomplete, since expanded paths under
035: collapsed ancestors cannot be accessed at all (without modifying the
036: expansion states, which doesn't work with vetos of TreeWillExpand-
037: Listeners). By listening to TreeExpansionEvents, this class mirrors
038: the expansion state for each path individually, independent from that
039: of its ancestors. It also listens to the TreeModel to remove paths
040: that have become invalid.
041: ExpansionStates are serializable if the TreePaths themselves are,
042: which they are if their components are. Typically you will want to
043: only serialize the state(), which doesn't also serialize the JTree
044: (If you wanted to serialize the JTree, you wouldn't need to the state
045: for serialization purposes at all.)
046:
047:
048: There are two ways to use this class:
049:
050: a) always have a ExpansionState around. Then the results will always be
051: completely right (and always accessible without a lot of overhead).
052:
053: Serializing/exporting:
054:
055: Collection state = cache.state(new HashSet());
056:
057: out.writeObject(state);
058:
059: When reading the state and creating the JTree, a new ExpansionState
060: is created:
061:
062: Set state = (Set)in.readObject();
063:
064: JTree tree = new JTree(data);
065:
066: ExpansionState cache = new ExpansionState(tree, state);
067:
068: Actually I don't like the side-effect of the constructor.
069:
070: Collections.EMPTY_SET can of course be used if there is no state yet.
071:
072: b) Only request the state on demand, and also restore it. This has less overhead
073: during execution, but a) has to modify the expansion structure while
074: trying to build the state, b) may actually confuse it
075: due to vetoes of TreeWillExpandListeners, and c) may give wrong results for
076: the same reason.
077:
078: Serializing/exporting:
079:
080: out.writeObject(ExpansionState.paths(tree, new HashSet()));
081:
082: Reading the state:
083:
084: Set state = (Set)in.readObject();
085:
086: JTree tree = new JTree(data);
087:
088: ExpansionState.setPaths(tree, state);
089:
090: Note the example code uses HashSet because setPaths() does (and very probably
091: always will) make use of contains(), which should thus be fast.
092: */
093: public class ExpansionState extends AbstractSet implements Serializable {
094: private JTree tree;
095:
096: private Set paths;
097:
098: private transient Listener listener;
099:
100: /** For the given JTree. Assumes only the root is expanded, if at all
101: (for example, a freshly created JTree, or one for which the model has
102: just been set)
103: */
104: public ExpansionState(JTree t) {
105: tree = t;
106:
107: paths = new HashSet();
108:
109: listener = createListener();
110:
111: tree.addPropertyChangeListener(listener);
112: tree.addTreeExpansionListener(listener);
113:
114: TreeModel data = tree.getModel();
115:
116: if (data != null) {
117: data.addTreeModelListener(listener);
118:
119: readFromTree();
120: }
121: }
122:
123: /** For the given JTree, with the given set of expanded paths.
124: This is equivalent to using the normal constructor, and then
125: calling setPaths(tree, state).
126: */
127: public ExpansionState(JTree tree, Collection state) {
128: this (tree, state, false);
129: }
130:
131: /** For the given JTree, with the given set of expanded paths.
132: This is equivalent to using the normal constructor, and then
133: calling setPaths(tree, state, false);
134: */
135: public ExpansionState(JTree tree, Collection state,
136: boolean assumeCollapsed) {
137: this (tree);
138:
139: setPaths(tree, state, assumeCollapsed);
140: }
141:
142: public void disconnect(JTree t) {
143: tree.removePropertyChangeListener(listener);
144: tree.removeTreeExpansionListener(listener);
145: TreeModel data = tree.getModel();
146: if (data != null)
147: data.removeTreeModelListener(listener);
148: }
149:
150: private void readFromTree() {
151: TreeModel data = tree.getModel();
152:
153: Object root = data.getRoot();
154:
155: if (root != null) {
156: TreePath rootPath = new TreePath(root);
157:
158: // This is a heuristic, we cannot truly capture all
159: // Unless someone has subclassed JTree, only the root
160: // will be expanded, if at all.
161: // It is much too expensive to really use paths()
162: // from below.
163:
164: if (tree.isExpanded(rootPath))
165: for (Enumeration e = tree
166: .getExpandedDescendants(rootPath); e
167: .hasMoreElements();)
168: paths.add(e.nextElement());
169: }
170: }
171:
172: public int size() {
173: return paths.size();
174: }
175:
176: public boolean isEmpty() {
177: return paths.isEmpty();
178: }
179:
180: public boolean contains(Object item) {
181: return paths.contains(item);
182: }
183:
184: public boolean containsAll(Collection c) {
185: return paths.containsAll(c);
186: }
187:
188: /**
189: Are all the ancestors (including the path) expanded?
190: */
191: public boolean containsAncestors(TreePath path) {
192: do {
193: if (!contains(path))
194: return false;
195:
196: path = path.getParentPath();
197:
198: } while (path != null);
199:
200: return true;
201: }
202:
203: /**
204: Are all the ancestors (including the paths) expanded?
205: */
206: public boolean containsAllAncestors(Collection c) {
207: for (Iterator i = c.iterator(); i.hasNext();)
208: if (!containsAncestors((TreePath) i.next()))
209: return false;
210:
211: return true;
212: }
213:
214: public Iterator iterator() {
215: return new Iterator() {
216: Iterator i = paths.iterator();
217:
218: public boolean hasNext() {
219: return i.hasNext();
220: }
221:
222: public Object next() {
223: return i.next();
224: }
225:
226: public void remove() {
227: throw new UnsupportedOperationException();
228: }
229: };
230: }
231:
232: protected Object clone() throws CloneNotSupportedException {
233: throw new CloneNotSupportedException();
234: }
235:
236: private void readObject(ObjectInputStream in) throws IOException,
237: ClassNotFoundException {
238: in.defaultReadObject();
239:
240: listener = createListener();
241:
242: tree.addPropertyChangeListener(listener);
243: tree.addTreeExpansionListener(listener);
244:
245: TreeModel data = tree.getModel();
246:
247: if (data != null) {
248: data.addTreeModelListener(listener);
249:
250: readFromTree();
251: }
252: }
253:
254: public Collection state(Collection result) {
255: result.clear();
256: result.addAll(paths);
257:
258: return result;
259: }
260:
261: /** Will re-expand the root if it was expanded and the tree has
262: an invisible root (otherwise the tree will appear empty, and there
263: is no easy way for the user to change that.
264: */
265: public static void collapseAll(JTree tree) {
266: TreeModel data = tree.getModel();
267:
268: if (data == null)
269: return;
270:
271: Object root = data.getRoot();
272:
273: if (root == null || data.isLeaf(root))
274: return;
275:
276: TreePath rootPath = new TreePath(root);
277:
278: boolean rootExpanded = tree.isExpanded(rootPath);
279:
280: collapseAll(tree, rootPath);
281:
282: if (rootExpanded && !tree.isRootVisible())
283: tree.expandPath(rootPath);
284: }
285:
286: /** requires: root is not a leaf. That implies that the tree's model is
287: not null and does have a root.
288: */
289: public static void collapseAll(JTree tree, TreePath root) {
290: collapseAllImpl(tree, tree.getModel(), root);
291: }
292:
293: private static void collapseAllImpl(JTree tree, TreeModel data,
294: TreePath path) {
295: Object node = path.getLastPathComponent();
296:
297: for (int count = data.getChildCount(node), i = 0; i < count; i++) {
298: Object child = data.getChild(node, i);
299:
300: if (!data.isLeaf(child))
301: collapseAllImpl(tree, data, path
302: .pathByAddingChild(child));
303: }
304:
305: // cannot check, since we cannot assume all ancestors
306: // are expanded
307: // afterwards they are, though, so the first walk could be handled
308: // special?
309: tree.collapsePath(path);
310: }
311:
312: public static void expandAll(JTree tree) {
313: TreeModel data = tree.getModel();
314:
315: if (data == null)
316: return;
317:
318: Object root = data.getRoot();
319:
320: if (root == null || data.isLeaf(root))
321: return;
322:
323: expandAll(tree, new TreePath(root));
324: }
325:
326: /** requires: path is not a leaf. That implies the tree has a model,
327: and that has a root.
328: */
329: public static void expandAll(JTree tree, TreePath path) {
330: for (Iterator i = extremalPaths(tree.getModel(), path,
331: new HashSet()).iterator(); i.hasNext();)
332: tree.expandPath((TreePath) i.next());
333: }
334:
335: /** The "extremal paths" of the tree model's subtree starting at
336: path. The extremal paths are those paths that a) are non-leaves
337: and b) have only leaf children, if any. It suffices to know
338: these to know all non-leaf paths in the subtree, and those are
339: the ones that matter for expansion (since the concept of expan-
340: sion only applies to non-leaves).
341: The extremal paths collection of a leave is empty.
342: The extremal paths are stored in the order in which they appear
343: in pre-order in the tree model.
344: */
345: private static Collection extremalPaths(TreeModel data,
346: TreePath path, Collection result) {
347: result.clear();
348:
349: if (data.isLeaf(path.getLastPathComponent()))
350: return result; // should really be forbidden (?)
351:
352: extremalPathsImpl(data, path, result);
353:
354: return result;
355: }
356:
357: private static void extremalPathsImpl(TreeModel data,
358: TreePath path, Collection result) {
359: Object node = path.getLastPathComponent();
360:
361: boolean hasNonLeafChildren = false;
362:
363: int count = data.getChildCount(node);
364:
365: for (int i = 0; i < count; i++)
366: if (!data.isLeaf(data.getChild(node, i)))
367: hasNonLeafChildren = true;
368:
369: if (!hasNonLeafChildren)
370: result.add(path);
371: else {
372: for (int i = 0; i < count; i++) {
373: Object child = data.getChild(node, i);
374:
375: if (!data.isLeaf(child))
376: extremalPathsImpl(data, path
377: .pathByAddingChild(child), result);
378: }
379: }
380: }
381:
382: /** All paths in the JTree that are expanded, including those
383: under hidden parents. The result is the same as if attaching
384: an ExpansionState to the JTree (in creation state) and then
385: calling state() on it.
386: To return the proper result, this method must temporarily
387: expand paths. If any TreeWillExpandListeners veto that, the
388: result is undefined.
389: */
390: public static Collection paths(JTree tree, Collection result) {
391: result.clear();
392:
393: TreeModel data = tree.getModel();
394:
395: if (data == null)
396: return result;
397:
398: Object root = data.getRoot();
399:
400: if (root == null || data.isLeaf(root))
401: return result;
402:
403: pathsImpl(tree, data, new TreePath(root), result);
404:
405: return result;
406: }
407:
408: private static void pathsImpl(JTree tree, TreeModel data,
409: TreePath path, Collection result) {
410: boolean expanded = tree.isExpanded(path);
411:
412: if (expanded)
413: result.add(path);
414: else
415: tree.expandPath(path);
416:
417: Object node = path.getLastPathComponent();
418:
419: for (int count = data.getChildCount(node), i = 0; i < count; i++) {
420: Object child = data.getChild(node, i);
421:
422: if (!data.isLeaf(child))
423: pathsImpl(tree, data, path.pathByAddingChild(child),
424: result);
425: }
426:
427: if (!expanded)
428: tree.collapsePath(path);
429: }
430:
431: /** Try to expand exactly the paths given in paths. Of course requires them to be
432: valid in the current TreeModel.
433: Will give undefined results if any TreeWillExpandListeners veto.
434: This implementation does not assume all paths are collapsed.
435: */
436: public static void setPaths(JTree tree, Collection paths) {
437: setPaths(tree, paths, false);
438: }
439:
440: /** assumedCollapsed: if true, assume that (if at all) only the root
441: is expanded. That way, the iteration over the tree nodes only goes
442: to the maximum level of the nodes in 'paths'.
443: */
444: public static void setPaths(JTree tree, Collection paths,
445: boolean assumeCollapsed) {
446: TreeModel data = tree.getModel();
447:
448: if (data == null)
449: return;
450:
451: Object root = data.getRoot();
452:
453: if (root == null || data.isLeaf(root))
454: return;
455:
456: if (assumeCollapsed) {
457: int maxLevel = 1; // always handle the root (doesn't really matter)
458:
459: for (Iterator i = paths.iterator(); i.hasNext();)
460: maxLevel = Math.max(maxLevel, ((TreePath) i.next())
461: .getPathCount());
462:
463: setPathsImpl(tree, data, new TreePath(root), maxLevel - 1,
464: paths);
465: } else
466: setPathsImpl(tree, data, new TreePath(root),
467: Integer.MAX_VALUE, paths);
468: }
469:
470: private static void setPathsImpl(JTree tree, TreeModel data,
471: TreePath path, int maxLevel, Collection paths) {
472: if (maxLevel > 0) {
473: Object node = path.getLastPathComponent();
474:
475: for (int count = data.getChildCount(node), i = 0; i < count; i++) {
476: Object child = data.getChild(node, i);
477:
478: if (!data.isLeaf(child))
479: setPathsImpl(tree, data, path
480: .pathByAddingChild(child), maxLevel - 1,
481: paths);
482: }
483: }
484:
485: // Since this is post-order, it doesn't matter that the ancestors are
486: // also expanded. They will be handled afterwards.
487: if (paths.contains(path)) {
488: if (!tree.isExpanded(path))
489: tree.expandPath(path);
490: } else {
491: // The ancestors are always expanded, so isCollapse() won't give
492: // wrong results.
493: if (!tree.isCollapsed(path))
494: tree.collapsePath(path);
495: }
496: }
497:
498: private Listener createListener() {
499: return new Listener();
500: }
501:
502: private class Listener implements TreeExpansionListener,
503: TreeModelListener, PropertyChangeListener {
504: public void propertyChange(PropertyChangeEvent e) {
505: if (e.getPropertyName().equals("model")) {
506: TreeModel old = (TreeModel) e.getOldValue();
507:
508: if (old != null)
509: old.removeTreeModelListener(this );
510:
511: paths.clear();
512:
513: TreeModel data = tree.getModel();
514:
515: if (data != null) {
516: data.addTreeModelListener(this );
517: readFromTree();
518: }
519: }
520: }
521:
522: public void treeExpanded(TreeExpansionEvent e) {
523: paths.add(e.getPath());
524: }
525:
526: public void treeCollapsed(TreeExpansionEvent e) {
527: paths.remove(e.getPath());
528: }
529:
530: public void treeNodesChanged(TreeModelEvent e) {
531: }
532:
533: public void treeNodesInserted(TreeModelEvent e) {
534: }
535:
536: public void treeNodesRemoved(TreeModelEvent e) {
537: TreePath parent = e.getTreePath();
538:
539: Object[] children = e.getChildren();
540:
541: for (int i = 0; i < children.length; i++)
542: removeDescendants(parent.pathByAddingChild(children[i]));
543: }
544:
545: public void treeStructureChanged(TreeModelEvent e) {
546: TreePath path = e.getTreePath();
547:
548: // Heuristic for new null root. It is undocumented which
549: // event really to expect.
550: if (path == null) {
551: paths.clear();
552: return;
553: }
554:
555: // new root, or root changed. JTree will maybe expand the root.
556: if (path.getParentPath() == null) {
557: paths.clear();
558: readFromTree();
559: } else {
560: removeDescendants(path);
561:
562: // PR
563: if (tree.isExpanded(path))
564: paths.add(path);
565: }
566: }
567:
568: // remove the descendants (which, by definition, include the path
569: // itself)
570: private void removeDescendants(TreePath path) {
571: for (Iterator i = paths.iterator(); i.hasNext();) {
572: TreePath current = (TreePath) i.next();
573:
574: if (current.isDescendant(path))
575: i.remove();
576: }
577: }
578: }
579: }
|