001: //Copyright (c) Janna Khegai 2004, Hans-Joachim Daniels 2005
002: //
003: //This program is free software; you can redistribute it and/or modify
004: //it under the terms of the GNU General Public License as published by
005: //the Free Software Foundation; either version 2 of the License, or
006: //(at your option) any later version.
007: //
008: //This program is distributed in the hope that it will be useful,
009: //but WITHOUT ANY WARRANTY; without even the implied warranty of
010: //MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
011: //GNU General Public License for more details.
012: //
013: //You can either finde the file LICENSE or LICENSE.TXT in the source
014: //distribution or in the .jar file of this application
015:
016: package de.uka.ilkd.key.ocl.gf;
017:
018: /*
019: * This code is based on an example provided by Richard Stanford,
020: * a tutorial reader.
021: */
022:
023: import java.awt.*;
024: import java.awt.event.*;
025: import java.util.logging.Level;
026: import java.util.logging.Logger;
027:
028: import javax.swing.JPanel;
029: import javax.swing.JScrollPane;
030: import javax.swing.JTree;
031: import javax.swing.ToolTipManager;
032: import javax.swing.event.TreeModelEvent;
033: import javax.swing.event.TreeModelListener;
034: import javax.swing.event.TreeSelectionEvent;
035: import javax.swing.event.TreeSelectionListener;
036: import javax.swing.tree.*;
037:
038: /**
039: * A GUI class, does store the tree, but does not create it.
040: * The tree is created in GFEditor2.
041: * This class displays the tree and let the user interact with it via mouse clicks.
042: */
043: public class DynamicTree2 extends JPanel implements KeyListener {
044: protected static Logger logger = Logger
045: .getLogger(DynamicTree2.class.getName());
046:
047: public DefaultMutableTreeNode rootNode;
048: private DefaultTreeModel treeModel;
049: public JTree tree;
050: private Toolkit toolkit = Toolkit.getDefaultToolkit();
051: private GFEditor2 gfeditor;
052: protected TreePath oldSelection = null;
053:
054: /**
055: * Initializes the display state of the tree panel, sets up the
056: * event handlers.
057: * Does not initialize the tree.
058: * @param gfe The editor object this object belongs to.
059: */
060: public DynamicTree2(GFEditor2 gfe) {
061:
062: this .gfeditor = gfe;
063: rootNode = new DefaultMutableTreeNode("Root Node");
064: treeModel = new DefaultTreeModel(rootNode);
065: treeModel.addTreeModelListener(new MyTreeModelListener());
066:
067: tree = new JTree(treeModel);
068: tree.setRootVisible(false);
069: tree.setEditable(false);
070: tree.getSelectionModel().setSelectionMode(
071: TreeSelectionModel.SINGLE_TREE_SELECTION);
072: tree.addKeyListener(this );
073:
074: //Add listener to components that can bring up popup menus.
075: MouseListener popupListener = new PopupListener();
076: tree.addMouseListener(popupListener);
077:
078: tree.addTreeSelectionListener(new TreeSelectionListener() {
079: /**
080: * Moves to the position of the selected node in GF.
081: * the following is assumed:
082: * gfeditor.nodeTable contains the positions for all selectionPathes.
083: */
084: public void valueChanged(TreeSelectionEvent e) {
085: if ((tree.getSelectionPath() != null)
086: && tree.getSelectionPath().equals(oldSelection)) {
087: //nothing to be done here, probably
088: //triggered by showTree
089: return;
090: }
091: if (tree.getSelectionRows() != null) {
092: if (tree.getSelectionPath() == null) {
093: if (logger.isLoggable(Level.FINER)) {
094: logger.finer("null root path");
095: }
096: } else {
097: if (logger.isLoggable(Level.FINER)) {
098: logger.finer("selected path"
099: + tree.getSelectionPath());
100: }
101: }
102: String pos = gfeditor.getNodePosition(tree
103: .getSelectionPath());
104: if (pos == null || "".equals(pos)) {
105: //default to sth. sensible
106: pos = "[]";
107: }
108: gfeditor.send("[t] mp " + pos);
109: }
110: oldSelection = tree.getSelectionPath();
111: }
112: });
113:
114: tree.setCellRenderer(new MyRenderer());
115: tree.setShowsRootHandles(true);
116: ToolTipManager.sharedInstance().registerComponent(tree);
117: ToolTipManager.sharedInstance().setDismissDelay(60000);
118: setPreferredSize(new Dimension(200, 100));
119: JScrollPane scrollPane = new JScrollPane(tree);
120: setLayout(new GridLayout(1, 0));
121: add(scrollPane);
122: }
123:
124: /**
125: * Remove all nodes in the tree and
126: * form a dummy tree in treePanel
127: */
128: protected void resetTree() {
129: ((DefaultTreeModel) (tree.getModel()))
130: .setRoot(new DefaultMutableTreeNode("Root"));
131: ((DefaultTreeModel) (tree.getModel())).reload();
132: }
133:
134: /** Remove all nodes except the root node. */
135: public void clear() {
136: ((DefaultTreeModel) (tree.getModel())).setRoot(null);
137: oldSelection = null;
138: //((DefaultTreeModel)(tree.getModel())).reload();
139: }
140:
141: /** Remove the currently selected node. */
142: public void removeCurrentNode() {
143: TreePath currentSelection = tree.getSelectionPath();
144: if (currentSelection != null) {
145: DefaultMutableTreeNode currentNode = (DefaultMutableTreeNode) (currentSelection
146: .getLastPathComponent());
147: MutableTreeNode parent = (MutableTreeNode) (currentNode
148: .getParent());
149: if (parent != null) {
150: treeModel.removeNodeFromParent(currentNode);
151: return;
152: }
153: }
154:
155: // Either there was no selection, or the root was selected.
156: toolkit.beep();
157: }
158:
159: /**
160: * Add child to the root node.
161: * It will come last in this node.
162: * @param child the payload of the new node
163: * @return the tree node having child as the node data
164: */
165: public DefaultMutableTreeNode addObject(Object child) {
166: DefaultMutableTreeNode parentNode = null;
167: TreePath parentPath = tree.getSelectionPath();
168:
169: if (parentPath == null) {
170: parentNode = rootNode;
171: } else {
172: parentNode = (DefaultMutableTreeNode) (parentPath
173: .getLastPathComponent());
174: }
175:
176: return addObject(parentNode, child, true);
177: }
178:
179: /**
180: * Add a new node containing child to the node parent.
181: * It will come last in this node.
182: * This method gets actually called
183: * @param parent the parent node of the to be created node
184: * @param child the wannabe node data
185: * @return the tree node having child as the node data and parent as the parent
186: */
187: public DefaultMutableTreeNode addObject(
188: DefaultMutableTreeNode parent, Object child) {
189: return addObject(parent, child, false);
190: }
191:
192: /**
193: * Add child to the currently selected node (parent?).
194: * It will come last in this node.
195: * @param parent the parent node of the to be created node
196: * @param child the wannabe node data
197: * @param shouldBeVisible true iff the viewport should show the
198: * new node afterwards
199: * @return the tree node having child as the node data and parent
200: * as the parent
201: */
202: public DefaultMutableTreeNode addObject(
203: DefaultMutableTreeNode parent, Object child,
204: boolean shouldBeVisible) {
205: if (logger.isLoggable(Level.FINER)) {
206: logger.finer("node added: '" + child + "', parent: '"
207: + parent + "'");
208: }
209: DefaultMutableTreeNode childNode = new DefaultMutableTreeNode(
210: child);
211:
212: if (parent == null) {
213: parent = rootNode;
214: }
215:
216: treeModel.insertNodeInto(childNode, parent, parent
217: .getChildCount());
218:
219: // Make sure the user can see the lovely new node.
220: if (shouldBeVisible) {
221: tree.scrollPathToVisible(new TreePath(childNode.getPath()));
222: }
223: return childNode;
224: }
225:
226: class MyTreeModelListener implements TreeModelListener {
227: public void treeNodesChanged(TreeModelEvent e) {
228: DefaultMutableTreeNode node;
229: node = (DefaultMutableTreeNode) (e.getTreePath()
230: .getLastPathComponent());
231:
232: /*
233: * If the event lists children, then the changed
234: * node is the child of the node we've already
235: * gotten. Otherwise, the changed node and the
236: * specified node are the same.
237: */
238: try {
239: int index = e.getChildIndices()[0];
240: node = (DefaultMutableTreeNode) (node.getChildAt(index));
241: } catch (NullPointerException exc) {
242: System.err.println(exc.getMessage());
243: exc.printStackTrace();
244: }
245:
246: if (logger.isLoggable(Level.FINER)) {
247: logger.finer("The user has finished editing the node.");
248: logger.finer("New value: " + node.getUserObject());
249: }
250: }
251:
252: public void treeNodesInserted(TreeModelEvent e) {
253: //nothing to be done here
254: }
255:
256: public void treeNodesRemoved(TreeModelEvent e) {
257: //nothing to be done here
258: }
259:
260: public void treeStructureChanged(TreeModelEvent e) {
261: //nothing to be done here
262: }
263: }
264:
265: /**
266: * This tree cell renderer got overwritten to make it possible to show
267: * tooltips according to the user object
268: */
269: private class MyRenderer extends DefaultTreeCellRenderer {
270: //int counter = 0;
271: //final ImageIcon iconFilled;
272: //final ImageIcon iconOpen;
273:
274: // public MyRenderer() {
275: // final URL urlOpen = KeYResourceManager.getManager().getResourceFile(DynamicTree2.class, "metal_leaf_open.png");
276: // final URL urlFilled = KeYResourceManager.getManager().getResourceFile(DynamicTree2.class, "metal_leaf_filled.png");
277: // iconOpen = new ImageIcon(urlOpen);
278: // iconFilled = new ImageIcon(urlFilled);
279: // }
280:
281: /**
282: * The heart of this class, sets display and tooltip text
283: * depending on the user data
284: */
285: public Component getTreeCellRendererComponent(JTree tree,
286: Object value, boolean sel, boolean expanded,
287: boolean leaf, int row, boolean hasFocus) {
288:
289: super .getTreeCellRendererComponent(tree, value, sel,
290: expanded, leaf, row, hasFocus);
291: if (value instanceof DefaultMutableTreeNode) {
292: DefaultMutableTreeNode node = (DefaultMutableTreeNode) value;
293: if (node.getUserObject() instanceof AstNodeData) {
294: AstNodeData and = (AstNodeData) node
295: .getUserObject();
296: String ptt = and.getParamTooltip();
297: if (!and.subtypingStatus) {
298: this .setForeground(Color.RED);
299: ptt = Printname
300: .htmlAppend(
301: ptt,
302: "<p>Subtyping proof is missing. <br>If no refinements are offered here, then there is a subtyping error.");
303: }
304: this .setToolTipText(ptt);
305: this .setText(and.toString());
306: // if (and.isMeta()) {
307: // this.setLeafIcon(this.iconOpen);
308: // } else {
309: // this.setLeafIcon(this.iconFilled);
310: // }
311: } else {
312: this .setToolTipText(null);
313: this .setText(value.toString());
314: }
315: } else {
316: this .setToolTipText(null);
317: this .setText(value.toString());
318: }
319: return this ;
320: }
321:
322: /**
323: * Checks if the current node represents an open metavariable
324: * or question mark
325: * @param value The payload of the node
326: * @return true iff value begins with a '?'
327: */
328: protected boolean isMetavariable(Object value) {
329: try {
330: DefaultMutableTreeNode node = (DefaultMutableTreeNode) value;
331: String nodeInfo = (String) (node.getUserObject());
332: if (nodeInfo.indexOf("?") == 0) {
333: return true;
334: }
335: } catch (Exception e) {
336: e.printStackTrace();
337: return false;
338: }
339:
340: return false;
341: }
342:
343: }//class
344:
345: class PopupListener extends MouseAdapter {
346: public void mousePressed(MouseEvent e) {
347: gfeditor.maybeShowPopup(e);
348: }
349:
350: public void mouseReleased(MouseEvent e) {
351: //nothing to be done here
352: }
353: }
354:
355: /**
356: * Handle the key pressed event.
357: */
358: public void keyPressed(KeyEvent e) {
359: int keyCode = e.getKeyCode();
360: switch (keyCode) {
361: case KeyEvent.VK_SPACE:
362: gfeditor.send("'");
363: break;
364: case KeyEvent.VK_DELETE:
365: gfeditor.send("d");
366: break;
367: }
368: }
369:
370: /**
371: * Handle the key typed event.
372: */
373: public void keyTyped(KeyEvent e) {
374: //nothing to be done here
375: }
376:
377: /**
378: * Handle the key released event.
379: */
380: public void keyReleased(KeyEvent e) {
381: //nothing to be done here
382: }
383:
384: }
|