Source Code Cross Referenced for GUIProofTreeModel.java in  » Testing » KeY » de » uka » ilkd » key » gui » prooftree » Java Source Code / Java DocumentationJava Source Code and Java Documentation

Java Source Code / Java Documentation
1. 6.0 JDK Core
2. 6.0 JDK Modules
3. 6.0 JDK Modules com.sun
4. 6.0 JDK Modules com.sun.java
5. 6.0 JDK Modules sun
6. 6.0 JDK Platform
7. Ajax
8. Apache Harmony Java SE
9. Aspect oriented
10. Authentication Authorization
11. Blogger System
12. Build
13. Byte Code
14. Cache
15. Chart
16. Chat
17. Code Analyzer
18. Collaboration
19. Content Management System
20. Database Client
21. Database DBMS
22. Database JDBC Connection Pool
23. Database ORM
24. Development
25. EJB Server geronimo
26. EJB Server GlassFish
27. EJB Server JBoss 4.2.1
28. EJB Server resin 3.1.5
29. ERP CRM Financial
30. ESB
31. Forum
32. GIS
33. Graphic Library
34. Groupware
35. HTML Parser
36. IDE
37. IDE Eclipse
38. IDE Netbeans
39. Installer
40. Internationalization Localization
41. Inversion of Control
42. Issue Tracking
43. J2EE
44. JBoss
45. JMS
46. JMX
47. Library
48. Mail Clients
49. Net
50. Parser
51. PDF
52. Portal
53. Profiler
54. Project Management
55. Report
56. RSS RDF
57. Rule Engine
58. Science
59. Scripting
60. Search Engine
61. Security
62. Sevlet Container
63. Source Control
64. Swing Library
65. Template Engine
66. Test Coverage
67. Testing
68. UML
69. Web Crawler
70. Web Framework
71. Web Mail
72. Web Server
73. Web Services
74. Web Services apache cxf 2.0.1
75. Web Services AXIS2
76. Wiki Engine
77. Workflow Engines
78. XML
79. XML UI
Java
Java Tutorial
Java Open Source
Jar File Download
Java Articles
Java Products
Java by API
Photoshop Tutorials
Maya Tutorials
Flash Tutorials
3ds-Max Tutorials
Illustrator Tutorials
GIMP Tutorials
C# / C Sharp
C# / CSharp Tutorial
C# / CSharp Open Source
ASP.Net
ASP.NET Tutorial
JavaScript DHTML
JavaScript Tutorial
JavaScript Reference
HTML / CSS
HTML CSS Reference
C / ANSI-C
C Tutorial
C++
C++ Tutorial
Ruby
PHP
Python
Python Tutorial
Python Open Source
SQL Server / T-SQL
SQL Server / T-SQL Tutorial
Oracle PL / SQL
Oracle PL/SQL Tutorial
PostgreSQL
SQL / MySQL
MySQL Tutorial
VB.Net
VB.Net Tutorial
Flash / Flex / ActionScript
VBA / Excel / Access / Word
XML
XML Tutorial
Microsoft Office PowerPoint 2007 Tutorial
Microsoft Office Excel 2007 Tutorial
Microsoft Office Word 2007 Tutorial
Java Source Code / Java Documentation » Testing » KeY » de.uka.ilkd.key.gui.prooftree 
Source Cross Referenced  Class Diagram Java Document (Java Doc) 


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:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.