| javax.swing.JPanel de.uka.ilkd.key.ocl.gf.DynamicTree2
DynamicTree2 | public class DynamicTree2 extends JPanel implements KeyListener(Code) | | A GUI class, does store the tree, but does not create it.
The tree is created in GFEditor2.
This class displays the tree and let the user interact with it via mouse clicks.
|
Constructor Summary | |
public | DynamicTree2(GFEditor2 gfe) Initializes the display state of the tree panel, sets up the
event handlers. |
DynamicTree2 | public DynamicTree2(GFEditor2 gfe)(Code) | | Initializes the display state of the tree panel, sets up the
event handlers.
Does not initialize the tree.
Parameters: gfe - The editor object this object belongs to. |
addObject | public DefaultMutableTreeNode addObject(Object child)(Code) | | Add child to the root node.
It will come last in this node.
Parameters: child - the payload of the new node the tree node having child as the node data |
addObject | public DefaultMutableTreeNode addObject(DefaultMutableTreeNode parent, Object child)(Code) | | Add a new node containing child to the node parent.
It will come last in this node.
This method gets actually called
Parameters: parent - the parent node of the to be created node Parameters: child - the wannabe node data the tree node having child as the node data and parent as the parent |
addObject | public DefaultMutableTreeNode addObject(DefaultMutableTreeNode parent, Object child, boolean shouldBeVisible)(Code) | | Add child to the currently selected node (parent?).
It will come last in this node.
Parameters: parent - the parent node of the to be created node Parameters: child - the wannabe node data Parameters: shouldBeVisible - true iff the viewport should show the new node afterwards the tree node having child as the node data and parent as the parent |
clear | public void clear()(Code) | | Remove all nodes except the root node.
|
keyPressed | public void keyPressed(KeyEvent e)(Code) | | Handle the key pressed event.
|
keyReleased | public void keyReleased(KeyEvent e)(Code) | | Handle the key released event.
|
keyTyped | public void keyTyped(KeyEvent e)(Code) | | Handle the key typed event.
|
removeCurrentNode | public void removeCurrentNode()(Code) | | Remove the currently selected node.
|
resetTree | protected void resetTree()(Code) | | Remove all nodes in the tree and
form a dummy tree in treePanel
|
|
|