| java.lang.Object
 java.util.AbstractCollection
java.util.AbstractSet
de.uka.ilkd.key.gui.prooftree.ExpansionState
| ExpansionState | | public class ExpansionState extends AbstractSet implements Serializable(Code) | | Cache/Access JTree's expansion state. The interface of JTree to access
the expanded paths is rather incomplete, since expanded paths under
collapsed ancestors cannot be accessed at all (without modifying the
expansion states, which doesn't work with vetos of TreeWillExpand-
Listeners). By listening to TreeExpansionEvents, this class mirrors
the expansion state for each path individually, independent from that
of its ancestors. It also listens to the TreeModel to remove paths
that have become invalid.
ExpansionStates are serializable if the TreePaths themselves are,
which they are if their components are. Typically you will want to
only serialize the state(), which doesn't also serialize the JTree
(If you wanted to serialize the JTree, you wouldn't need to the state
for serialization purposes at all.)
There are two ways to use this class:
a) always have a ExpansionState around. Then the results will always be
completely right (and always accessible without a lot of overhead).
Serializing/exporting:
Collection state = cache.state(new HashSet());
out.writeObject(state);
When reading the state and creating the JTree, a new ExpansionState
is created:
Set state = (Set)in.readObject();
JTree tree = new JTree(data);
ExpansionState cache = new ExpansionState(tree, state);
Actually I don't like the side-effect of the constructor.
Collections.EMPTY_SET can of course be used if there is no state yet.
b) Only request the state on demand, and also restore it. This has less overhead
during execution, but a) has to modify the expansion structure while
trying to build the state, b) may actually confuse it
due to vetoes of TreeWillExpandListeners, and c) may give wrong results for
the same reason.
Serializing/exporting:
out.writeObject(ExpansionState.paths(tree, new HashSet()));
Reading the state:
Set state = (Set)in.readObject();
JTree tree = new JTree(data);
ExpansionState.setPaths(tree, state);
Note the example code uses HashSet because setPaths() does (and very probably
always will) make use of contains(), which should thus be fast.
|
| ExpansionState | | public ExpansionState(JTree t)(Code) | | For the given JTree. Assumes only the root is expanded, if at all
(for example, a freshly created JTree, or one for which the model has
just been set)
|
| ExpansionState | | public ExpansionState(JTree tree, Collection state)(Code) | | For the given JTree, with the given set of expanded paths.
This is equivalent to using the normal constructor, and then
calling setPaths(tree, state).
|
| ExpansionState | | public ExpansionState(JTree tree, Collection state, boolean assumeCollapsed)(Code) | | For the given JTree, with the given set of expanded paths.
This is equivalent to using the normal constructor, and then
calling setPaths(tree, state, false);
|
| collapseAll | | public static void collapseAll(JTree tree)(Code) | | Will re-expand the root if it was expanded and the tree has
an invisible root (otherwise the tree will appear empty, and there
is no easy way for the user to change that.
|
| collapseAll | | public static void collapseAll(JTree tree, TreePath root)(Code) | | requires: root is not a leaf. That implies that the tree's model is
not null and does have a root.
|
| containsAllAncestors | | public boolean containsAllAncestors(Collection c)(Code) | | Are all the ancestors (including the paths) expanded?
|
| containsAncestors | | public boolean containsAncestors(TreePath path)(Code) | | Are all the ancestors (including the path) expanded?
|
| expandAll | | public static void expandAll(JTree tree)(Code) | | |
| expandAll | | public static void expandAll(JTree tree, TreePath path)(Code) | | requires: path is not a leaf. That implies the tree has a model,
and that has a root.
|
| isEmpty | | public boolean isEmpty()(Code) | | |
| paths | | public static Collection paths(JTree tree, Collection result)(Code) | | All paths in the JTree that are expanded, including those
under hidden parents. The result is the same as if attaching
an ExpansionState to the JTree (in creation state) and then
calling state() on it.
To return the proper result, this method must temporarily
expand paths. If any TreeWillExpandListeners veto that, the
result is undefined.
|
| setPaths | | public static void setPaths(JTree tree, Collection paths)(Code) | | Try to expand exactly the paths given in paths. Of course requires them to be
valid in the current TreeModel.
Will give undefined results if any TreeWillExpandListeners veto.
This implementation does not assume all paths are collapsed.
|
| setPaths | | public static void setPaths(JTree tree, Collection paths, boolean assumeCollapsed)(Code) | | assumedCollapsed: if true, assume that (if at all) only the root
is expanded. That way, the iteration over the tree nodes only goes
to the maximum level of the nodes in 'paths'.
|
|
|