Source Code Cross Referenced for ProofVisualizationView.java in  » Testing » KeY » proofVisualization » views » 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 » proofVisualization.views 
Source Cross Referenced  Class Diagram Java Document (Java Doc) 


001:        package proofVisualization.views;
002:
003:        import java.net.URL;
004:        import java.util.ArrayList;
005:        import java.util.HashSet;
006:        import java.util.Iterator;
007:        import java.util.LinkedList;
008:
009:        import org.eclipse.core.resources.IFile;
010:        import org.eclipse.core.resources.IWorkspaceRoot;
011:        import org.eclipse.core.resources.ResourcesPlugin;
012:        import org.eclipse.core.runtime.IPath;
013:        import org.eclipse.core.runtime.Path;
014:        import org.eclipse.core.runtime.Platform;
015:        import org.eclipse.jface.action.Action;
016:        import org.eclipse.jface.action.IMenuListener;
017:        import org.eclipse.jface.action.IMenuManager;
018:        import org.eclipse.jface.action.IToolBarManager;
019:        import org.eclipse.jface.action.MenuManager;
020:        import org.eclipse.jface.action.Separator;
021:        import org.eclipse.jface.dialogs.MessageDialog;
022:        import org.eclipse.jface.resource.ImageDescriptor;
023:        import org.eclipse.jface.text.BadLocationException;
024:        import org.eclipse.jface.text.ITextOperationTarget;
025:        import org.eclipse.jface.text.Position;
026:        import org.eclipse.jface.text.source.Annotation;
027:        import org.eclipse.jface.text.source.ISourceViewer;
028:        import org.eclipse.jface.viewers.DoubleClickEvent;
029:        import org.eclipse.jface.viewers.IDoubleClickListener;
030:        import org.eclipse.jface.viewers.ISelection;
031:        import org.eclipse.jface.viewers.ISelectionChangedListener;
032:        import org.eclipse.jface.viewers.IStructuredContentProvider;
033:        import org.eclipse.jface.viewers.IStructuredSelection;
034:        import org.eclipse.jface.viewers.ITreeContentProvider;
035:        import org.eclipse.jface.viewers.LabelProvider;
036:        import org.eclipse.jface.viewers.SelectionChangedEvent;
037:        import org.eclipse.jface.viewers.StructuredSelection;
038:        import org.eclipse.jface.viewers.TreeViewer;
039:        import org.eclipse.jface.viewers.Viewer;
040:        import org.eclipse.jface.viewers.ViewerSorter;
041:        import org.eclipse.swt.SWT;
042:        import org.eclipse.swt.graphics.Image;
043:        import org.eclipse.swt.widgets.Composite;
044:        import org.eclipse.swt.widgets.Menu;
045:        import org.eclipse.ui.IActionBars;
046:        import org.eclipse.ui.IEditorPart;
047:        import org.eclipse.ui.ISharedImages;
048:        import org.eclipse.ui.IWorkbench;
049:        import org.eclipse.ui.IWorkbenchActionConstants;
050:        import org.eclipse.ui.IWorkbenchPage;
051:        import org.eclipse.ui.PlatformUI;
052:        import org.eclipse.ui.part.DrillDownAdapter;
053:        import org.eclipse.ui.part.ViewPart;
054:        import org.osgi.framework.Bundle;
055:
056:        import proofVisualization.ProofVisualizationPlugin;
057:
058:        import de.uka.ilkd.key.gui.Main;
059:        import de.uka.ilkd.key.java.SourceElement;
060:        import de.uka.ilkd.key.java.PositionInfo;
061:        import de.uka.ilkd.key.java.declaration.LocalVariableDeclaration;
062:        import de.uka.ilkd.key.java.statement.LoopStatement;
063:        import de.uka.ilkd.key.visualization.ContextTraceElement;
064:        import de.uka.ilkd.key.visualization.ExecutionTraceModel;
065:        import de.uka.ilkd.key.visualization.ParentContextTraceElement;
066:        import de.uka.ilkd.key.visualization.ProofVisualization;
067:        import de.uka.ilkd.key.visualization.TraceElement;
068:        import de.uka.ilkd.key.visualization.VisualizationModel;
069:
070:        public class ProofVisualizationView extends ViewPart {
071:            private TreeViewer viewer;
072:
073:            private DrillDownAdapter drillDownAdapter;
074:            private Action visualizeNodeAction;
075:            private Action markNodeAction;
076:            private Action toNodeAction;
077:            private Action doubleClickAction;
078:            private Action rmAnnotationsAction;
079:            private Action stepIntoAction, stepOverAction;
080:
081:            private ParentContextTraceElement invisibleRoot;
082:            private ExecutionTraceModel trace;
083:            private VisualizationModel visualizationModel = null;
084:            private LinkedList sViewerList = new LinkedList();
085:
086:            private static String MARKER = "ProofVisualization.PVAnnotationType";
087:            private static String LAST_MARKER = "ProofVisualization.PVAnnotationType2";
088:            private static String EXC_MARKER = "ProofVisualization.PVAnnotationType3";
089:
090:            class ViewContentProvider implements  IStructuredContentProvider,
091:                    ITreeContentProvider {
092:
093:                public void inputChanged(Viewer v, Object oldInput,
094:                        Object newInput) {
095:                }
096:
097:                public void dispose() {
098:                }
099:
100:                public Object[] getElements(Object parent) {
101:                    if (parent.equals(getViewSite())) {
102:                        if (invisibleRoot == null)
103:                            initialize();
104:                        return getChildren(invisibleRoot);
105:                    }
106:                    return getChildren(parent);
107:                }
108:
109:                public Object getParent(Object child) {
110:                    if (child instanceof  TraceElement) {
111:                        if (((ContextTraceElement) child).getParent() == TraceElement.PARENTROOT)
112:                            return invisibleRoot;
113:                        return ((ContextTraceElement) child).getParent();
114:                    }
115:                    return null;
116:                }
117:
118:                public Object[] getChildren(Object parent) {
119:                    if (parent == invisibleRoot)
120:                        return collectTopLevelElements(invisibleRoot);
121:                    if (parent instanceof  ParentContextTraceElement)
122:                        return ((ParentContextTraceElement) parent)
123:                                .getChildren();
124:                    return new Object[0];
125:                }
126:
127:                private Object[] collectTopLevelElements(
128:                        ParentContextTraceElement root) {
129:                    ArrayList children = new ArrayList();
130:                    ContextTraceElement che = root.getNextExecuted();
131:                    while ((che != TraceElement.END)
132:                            && (TraceElement.PARENTROOT == che.getParent())) {
133:                        children.add(che);
134:                        if (che instanceof  ParentContextTraceElement)
135:                            che = ((ParentContextTraceElement) che).stepOver();
136:                        else
137:                            che = che.getNextExecuted();
138:                    }
139:                    return children.toArray();
140:                }
141:
142:                public boolean hasChildren(Object parent) {
143:                    return (parent instanceof  ParentContextTraceElement)
144:                            && ((ParentContextTraceElement) parent)
145:                                    .getChildren().length > 0;
146:                }
147:
148:                private void initialize() {
149:                    invisibleRoot = new ParentContextTraceElement();
150:                }
151:
152:            }
153:
154:            class ViewLabelProvider extends LabelProvider {
155:
156:                private String getTreeLabel(ContextTraceElement cte) {
157:                    String s = cte.getSrcElement().toString();
158:                    if (cte.getContextStatement() != null)
159:                        s = cte.getContextStatement().toString();
160:                    int i = s.indexOf("\n");
161:                    if (i > -1)
162:                        return s.substring(0, i);
163:                    return s;
164:                }
165:
166:                public String getText(Object obj) {
167:                    if (obj instanceof  ContextTraceElement)
168:                        return getTreeLabel((ContextTraceElement) obj);
169:                    return "unknown tree content";
170:                }
171:
172:                public Image getImage(Object obj) {
173:                    String imageKey = null;//ISharedImages.IMG_OBJ_ELEMENT;
174:                    if ((((TraceElement) obj).serialNr() == trace
175:                            .getLastContextTraceElement().serialNr())
176:                            && trace.uncaughtException())
177:                        return PlatformUI.getWorkbench().getSharedImages()
178:                                .getImage(ISharedImages.IMG_OBJS_ERROR_TSK);
179:                    if (obj instanceof  ParentContextTraceElement) {
180:                        imageKey = ISharedImages.IMG_OBJ_FOLDER;
181:                        return PlatformUI.getWorkbench().getSharedImages()
182:                                .getImage(imageKey);
183:                    }
184:                    return null;
185:                }
186:            }
187:
188:            class NameSorter extends ViewerSorter {
189:                public int compare(Viewer viewer, Object o1, Object o2) {
190:                    if (!(o1 instanceof  TraceElement)
191:                            || !(o2 instanceof  TraceElement))
192:                        return 0;
193:                    TraceElement h1 = (TraceElement) o1;
194:                    TraceElement h2 = (TraceElement) o2;
195:                    return h1.serialNr() - h2.serialNr();
196:                }
197:            }
198:
199:            public ProofVisualizationView() {
200:            }
201:
202:            /**
203:             * This is a callback that will allow us
204:             * to create the viewer and initialize it.
205:             */
206:            public void createPartControl(Composite parent) {
207:                viewer = new TreeViewer(parent, SWT.MULTI | SWT.H_SCROLL
208:                        | SWT.V_SCROLL);
209:                drillDownAdapter = new DrillDownAdapter(viewer);
210:                viewer.setContentProvider(new ViewContentProvider());
211:                viewer.setLabelProvider(new ViewLabelProvider());
212:                viewer.setSorter(new NameSorter());
213:                viewer.setInput(getViewSite());
214:                viewer
215:                        .addSelectionChangedListener(new ISelectionChangedListener() {
216:                            public void selectionChanged(
217:                                    SelectionChangedEvent event) {
218:
219:                            }
220:                        });
221:                hookListener();
222:                makeActions();
223:                hookContextMenu();
224:                hookDoubleClickAction();
225:                contributeToActionBars();
226:            }
227:
228:            private void hookListener() {
229:                viewer
230:                        .addSelectionChangedListener(new ISelectionChangedListener() {
231:                            public void selectionChanged(
232:                                    SelectionChangedEvent event) {
233:                                // if the selection is empty clear the label
234:                                if (event.getSelection().isEmpty()) {
235:
236:                                    return;
237:                                }
238:                                if (event.getSelection() instanceof  IStructuredSelection) {
239:                                    IStructuredSelection selection = (IStructuredSelection) event
240:                                            .getSelection();
241:                                    for (Iterator iterator = selection
242:                                            .iterator(); iterator.hasNext();) {
243:                                        removeAnnotionMarkers();
244:                                        Object domain = iterator.next();
245:                                        if (domain instanceof  ContextTraceElement)
246:                                            visualizeTraceElement(
247:                                                    (ContextTraceElement) domain,
248:                                                    false);
249:                                    }
250:                                }
251:                            }
252:                        });
253:            }
254:
255:            private void hookContextMenu() {
256:                MenuManager menuMgr = new MenuManager("#PopupMenu");
257:                menuMgr.setRemoveAllWhenShown(true);
258:                menuMgr.addMenuListener(new IMenuListener() {
259:                    public void menuAboutToShow(IMenuManager manager) {
260:                        ProofVisualizationView.this .fillContextMenu(manager);
261:                    }
262:                });
263:                Menu menu = menuMgr.createContextMenu(viewer.getControl());
264:                viewer.getControl().setMenu(menu);
265:                getSite().registerContextMenu(menuMgr, viewer);
266:            }
267:
268:            private void contributeToActionBars() {
269:                IActionBars bars = getViewSite().getActionBars();
270:                fillLocalPullDown(bars.getMenuManager());
271:                fillLocalToolBar(bars.getToolBarManager());
272:            }
273:
274:            private void fillLocalPullDown(IMenuManager manager) {
275:                manager.add(visualizeNodeAction);
276:                manager.add(new Separator());
277:                manager.add(rmAnnotationsAction);
278:            }
279:
280:            private void fillContextMenu(IMenuManager manager) {
281:                manager.add(toNodeAction);
282:                drillDownAdapter.addNavigationActions(manager);
283:                // Other plug-ins can contribute there actions here
284:                manager.add(new Separator(
285:                        IWorkbenchActionConstants.MB_ADDITIONS));
286:            }
287:
288:            private void fillLocalToolBar(IToolBarManager manager) {
289:                manager.add(new Separator());
290:                manager.add(stepIntoAction);
291:                manager.add(new Separator());
292:                manager.add(stepOverAction);
293:                manager.add(new Separator());
294:                manager.add(markNodeAction);
295:                manager.add(new Separator());
296:                manager.add(rmAnnotationsAction);
297:                manager.add(new Separator());
298:                manager.add(visualizeNodeAction);
299:                manager.add(new Separator());
300:                drillDownAdapter.addNavigationActions(manager);
301:            }
302:
303:            private int lineInfo(SourceElement se) {
304:                final PositionInfo pi = se.getPositionInfo();
305:                int line = pi.getStartPosition().getLine();
306:                // TODO line information of local variable declaration is
307:                // wrong. bug in recoder?
308:
309:                if (se instanceof  LocalVariableDeclaration) {
310:                    if (se.getEndPosition().getLine() > line) {
311:                        line++;
312:                    }
313:                }
314:
315:                return line - 1;
316:            }
317:
318:            private void makeVisible(TraceElement he) {
319:                ISourceViewer viewer = getSourceViewer(he.getSrcElement()
320:                        .getPositionInfo().getFileName());
321:                if (viewer == null)
322:                    return;
323:                int line = lineInfo(he.getSrcElement());
324:
325:                int sl = 0;
326:                int s2 = 1;
327:                try {
328:                    sl = viewer.getDocument().getLineOffset(line);
329:                    s2 = viewer.getDocument().getLineLength(line);
330:                } catch (BadLocationException e) {
331:                }
332:                viewer.revealRange(sl, s2);
333:            }
334:
335:            private void visualize(ContextTraceElement start,
336:                    ContextTraceElement end) {
337:                ContextTraceElement currentHe = start;
338:                LinkedList reverse = new LinkedList();
339:                while (currentHe != end) {
340:                    reverse.addFirst(currentHe);
341:                    currentHe = currentHe.getNextExecuted();
342:
343:                }
344:                if (currentHe != TraceElement.END)
345:                    reverse.addFirst(currentHe);
346:                HashSet visualized = new HashSet();
347:                boolean last = true;
348:                Iterator it = reverse.iterator();
349:                ContextTraceElement cte = TraceElement.END;
350:                while (it.hasNext()) {
351:                    cte = (ContextTraceElement) it.next();
352:                    if (!visualized.contains(cte.getSrcElement()
353:                            .getPositionInfo())) {
354:                        if (last)
355:                            visualizeTraceElement(cte, true);
356:                        else
357:                            visualizeTraceElement(cte, false);
358:                        last = false;
359:                        visualized.add(cte.getSrcElement().getPositionInfo());
360:                    }
361:                }
362:                if (cte != TraceElement.END)
363:                    makeVisible(cte);
364:            }
365:
366:            public ExecutionTraceModel getModelSelection(
367:                    VisualizationModel model) {
368:                ModelSelectionDialog dialog = new ModelSelectionDialog(
369:                        ProofVisualizationPlugin.getDefault().getWorkbench()
370:                                .getActiveWorkbenchWindow().getShell(), model);
371:                dialog.setTitle("Proof Visualization");
372:                dialog.setMessage("Select an execution trace");
373:                dialog.open();
374:                return (ExecutionTraceModel) (dialog.getResult()[0]);
375:            }
376:
377:            private void makeActions() {
378:                visualizeNodeAction = new Action() {
379:                    public void run() {
380:
381:                        ProofVisualization proofVis = Main.getInstance()
382:                                .mediator().visualizeProof();
383:                        if (proofVis != null) {
384:
385:                            if (proofVis.getVisualizationModel()
386:                                    .getExecutionTraces().length == 0) {
387:                                showMessage("No program executed on the branch so far.");
388:                            } else {
389:                                visualizationModel = proofVis
390:                                        .getVisualizationModel();
391:
392:                                if (visualizationModel.getExecutionTraces().length > 1) {
393:                                    ExecutionTraceModel selection = getModelSelection(visualizationModel);
394:                                    if (selection != null) {
395:                                        trace = selection;
396:                                        toNodeAction.setEnabled(true);
397:                                    } else
398:                                        trace = null;
399:                                } else {
400:                                    toNodeAction.setEnabled(true);
401:                                    trace = (visualizationModel
402:                                            .getExecutionTraces())[0];
403:                                }
404:                                removeAnnotionMarkers();
405:                                if (trace.getFirstContextTraceElement() != TraceElement.END) {
406:                                    visualize(trace
407:                                            .getFirstContextTraceElement(),
408:                                            TraceElement.END);
409:                                    setUpTree(trace
410:                                            .getFirstContextTraceElement());
411:                                    viewer
412:                                            .setExpandedElements(trace
413:                                                    .getPath(trace
414:                                                            .getLastContextTraceElement()));
415:                                    stepOverAction.setEnabled(true);
416:                                    stepIntoAction.setEnabled(true);
417:                                    markNodeAction.setEnabled(true);
418:
419:                                }
420:                            }
421:                        } else
422:                            showMessage("No Proof Loaded");
423:                    }
424:                };
425:                visualizeNodeAction.setText("Show Execution Traces");
426:                visualizeNodeAction
427:                        .setToolTipText("Shows the execution traces for the current selected node in the KeY-Prover");
428:                visualizeNodeAction.setImageDescriptor(ImageDescriptor
429:                        .createFromFile(this .getClass(), "visualize.png"));
430:                visualizeNodeAction.setImageDescriptor(null);
431:
432:                markNodeAction = new Action() {
433:                    public void run() {
434:                        ProofVisualization proofVis = Main.getInstance()
435:                                .mediator().visualizeProof();
436:                        if (proofVis != null) {
437:                            removeAnnotionMarkers();
438:                            visualize(trace.getFirstContextTraceElement(),
439:                                    TraceElement.END);
440:                        } else
441:                            showMessage("No Proof Loaded");
442:                    }
443:                };
444:                markNodeAction.setText("Mark All Statements");
445:                markNodeAction
446:                        .setToolTipText("Marks all statements of the execution trace in the Java editor");
447:                markNodeAction.setImageDescriptor(null);
448:
449:                toNodeAction = new Action() {
450:                    public void run() {
451:                        ISelection selection = viewer.getSelection();
452:                        Object obj = ((IStructuredSelection) selection)
453:                                .getFirstElement();
454:                        TraceElement he = (TraceElement) obj;
455:                        Main.getInstance().mediator().getSelectionModel()
456:                                .setSelectedNode(he.node());
457:                    }
458:                };
459:                toNodeAction.setText("Select associated Node");
460:                toNodeAction.setEnabled(false);
461:                toNodeAction
462:                        .setToolTipText("Selects the the associated Node in the KeY-Prover");
463:                toNodeAction.setImageDescriptor(PlatformUI.getWorkbench()
464:                        .getSharedImages().getImageDescriptor(
465:                                ISharedImages.IMG_DEF_VIEW));
466:
467:                rmAnnotationsAction = new Action() {
468:                    public void run() {
469:                        removeAnnotionMarkers();
470:                    }
471:                };
472:                rmAnnotationsAction.setText("Remove all Markers");
473:                rmAnnotationsAction
474:                        .setToolTipText("Removes all Proof Visualizuation Markers in the Java Editor");
475:                rmAnnotationsAction.setImageDescriptor(PlatformUI
476:                        .getWorkbench().getSharedImages().getImageDescriptor(
477:                                ISharedImages.IMG_TOOL_DELETE));
478:
479:                stepIntoAction = new Action() {
480:                    public void run() {
481:                        IStructuredSelection selection = (IStructuredSelection) viewer
482:                                .getSelection();
483:                        for (Iterator iterator = selection.iterator(); iterator
484:                                .hasNext();) {
485:                            Object domain = iterator.next();
486:                            if (domain instanceof  ContextTraceElement) {
487:                                ContextTraceElement cte = (ContextTraceElement) domain;
488:                                if (cte.getNextExecuted() != TraceElement.END) {
489:                                    viewer
490:                                            .setSelection(new StructuredSelection(
491:                                                    cte.getNextExecuted()));
492:                                }
493:                            }
494:                        }
495:                    }
496:                };
497:                stepIntoAction
498:                        .setToolTipText("Marks the next executed statement");
499:                stepIntoAction
500:                        .setImageDescriptor(getImageDescriptor("stepinto_co.gif"));
501:
502:                stepOverAction = new Action() {
503:                    public void run() {
504:                        IStructuredSelection selection = (IStructuredSelection) viewer
505:                                .getSelection();
506:                        for (Iterator iterator = selection.iterator(); iterator
507:                                .hasNext();) {
508:                            Object domain = iterator.next();
509:                            if (domain instanceof  ParentContextTraceElement) {
510:                                ParentContextTraceElement pcte = (ParentContextTraceElement) domain;
511:                                if (pcte.stepOver() != TraceElement.END) {
512:                                    viewer
513:                                            .setSelection(new StructuredSelection(
514:                                                    pcte.stepOver()));
515:                                }
516:                            } else if (domain instanceof  ContextTraceElement) {
517:                                ContextTraceElement cte = (ContextTraceElement) domain;
518:                                if (cte.getNextExecuted() != TraceElement.END) {
519:                                    viewer
520:                                            .setSelection(new StructuredSelection(
521:                                                    cte.getNextExecuted()));
522:                                }
523:                            }
524:                        }
525:                    }
526:                };
527:                stepOverAction
528:                        .setToolTipText("Step Over: Marks the next executed statement and"
529:                                + " jumps over substatements and method calls");
530:                stepOverAction
531:                        .setImageDescriptor(getImageDescriptor("stepover_co.gif"));
532:                doubleClickAction = new Action() {
533:                    public void run() {
534:                        ISelection selection = viewer.getSelection();
535:                        Object obj = ((IStructuredSelection) selection)
536:                                .getFirstElement();
537:                        ContextTraceElement cte = (ContextTraceElement) obj;
538:                        removeAnnotionMarkers();
539:                        visualize(trace.getFirstContextTraceElement(), cte);
540:                    }
541:                };
542:
543:                stepOverAction.setEnabled(false);
544:                stepIntoAction.setEnabled(false);
545:                markNodeAction.setEnabled(false);
546:            }
547:
548:            private ImageDescriptor getImageDescriptor(String file) {
549:                ImageDescriptor image = null;
550:                try {
551:                    String filename = "icons/" + file;
552:                    Bundle bun = Platform.getBundle("ProofVisualization");
553:                    IPath ip = new Path(filename);
554:                    URL url = Platform.find(bun, ip);
555:
556:                    URL resolved = Platform.resolve(url);
557:
558:                    image = ImageDescriptor.createFromURL(resolved);
559:                } catch (Exception e) {
560:                    e.printStackTrace();
561:                }
562:                return image;
563:            }
564:
565:            private void hookDoubleClickAction() {
566:                viewer.addDoubleClickListener(new IDoubleClickListener() {
567:                    public void doubleClick(DoubleClickEvent event) {
568:                        doubleClickAction.run();
569:                    }
570:                });
571:
572:            }
573:
574:            private void showMessage(String message) {
575:                MessageDialog.openInformation(viewer.getControl().getShell(),
576:                        "Proof Visualization", message);
577:            }
578:
579:            public void setUpTree(ContextTraceElement cte) {
580:                invisibleRoot.setStepInto(cte);
581:                viewer.refresh();
582:            }
583:
584:            public void removeAnnotionMarkers() {
585:                Object[] viewers = sViewerList.toArray();
586:                for (int i = 0; i < viewers.length; i++) {
587:                    ISourceViewer viewer = (ISourceViewer) viewers[i];
588:                    if (viewer == null)
589:                        continue;
590:                    Iterator iterator = viewer.getAnnotationModel()
591:                            .getAnnotationIterator();
592:                    while (iterator.hasNext()) {
593:                        Annotation ann = (Annotation) iterator.next();
594:                        if (ann instanceof  PVAnnotation)
595:                            viewer.getAnnotationModel().removeAnnotation(ann);
596:                    }
597:                }
598:                sViewerList = new LinkedList();
599:            }
600:
601:            public ISourceViewer getSourceViewer(String file) {
602:                IWorkspaceRoot myWorkspaceRoot = ResourcesPlugin.getWorkspace()
603:                        .getRoot();
604:
605:                // TODO find the eclipse project of  the  proof 
606:
607:                // This is a workaround, but
608:                // findFilesforLocations does not work with linked folders. 
609:                // See Bug 128460 at https://bugs.eclipse.org/
610:                // Bug is fixed in Stable Build: 3.2M5a
611:
612:                IFile[] f = myWorkspaceRoot
613:                        .findFilesForLocation(new Path(file));//pr.getFile(file);
614:                ISourceViewer viewer = null;
615:                IWorkbench workbench = PlatformUI.getWorkbench();
616:                IWorkbenchPage page = workbench.getActiveWorkbenchWindow()
617:                        .getActivePage();
618:                try {
619:                    IEditorPart ed = org.eclipse.ui.ide.IDE.openEditor(page,
620:                            f[0]);
621:                    viewer = (ISourceViewer) ed
622:                            .getAdapter(ITextOperationTarget.class);
623:                } catch (Exception e) {
624:                    e.printStackTrace();
625:                    return null;
626:                }
627:                return viewer;
628:            }
629:
630:            public void visualizeTraceElement(ContextTraceElement cte,
631:                    boolean last) {
632:                ISourceViewer viewer = getSourceViewer(cte.getSrcElement()
633:                        .getPositionInfo().getFileName());
634:                if (viewer == null)
635:                    return;
636:                if (!sViewerList.contains(viewer))
637:                    sViewerList.add(viewer);
638:
639:                int line = lineInfo(cte.getSrcElement());
640:
641:                if (!last) {
642:                    setAnnotationMarker(viewer, cte, getMessage(cte), MARKER,
643:                            line);
644:                } else {
645:                    setAnnotationMarker(viewer, cte, getMessage(cte),
646:                            LAST_MARKER, line);
647:
648:                }
649:                if (cte.getLabel() != null && (cte.getLabel().length() > 0)) {
650:                    setAnnotationMarker(viewer, cte, cte.getLabel(), MARKER,
651:                            line);
652:                }
653:
654:                if (cte == trace.getLastContextTraceElement()
655:                        && trace.uncaughtException())
656:                    setAnnotationMarker(viewer, cte, "Uncaught Exception: "
657:                            + trace.getUncaughtException().getSrcElement(),
658:                            EXC_MARKER, line);
659:
660:            }
661:
662:            public void setAnnotationMarker(ISourceViewer viewer,
663:                    ContextTraceElement he, String message, String type,
664:                    int line) {
665:                int s1 = 0;
666:                int s2 = 1;
667:                try {
668:                    s1 = viewer.getDocument().getLineOffset(line);
669:                    s2 = viewer.getDocument().getLineLength(line);
670:                } catch (BadLocationException e) {
671:                    e.printStackTrace();
672:                }
673:
674:                viewer.getAnnotationModel().addAnnotation(
675:                        new PVAnnotation(type, false, he, message),
676:                        new Position(s1, s2));
677:                viewer.revealRange(s1, s2);
678:            }
679:
680:            public String getMessage(ContextTraceElement he) {
681:                String s = "";
682:                if (he.getParent().getSrcElement() instanceof  LoopStatement) {
683:                    if (he.getNumberOfExecutions() > 1)
684:                        s += "Unwound: " + he.getNumberOfExecutions()
685:                                + " times";
686:                    else if (he.getNumberOfExecutions() == 1)
687:                        s += "Unwound: " + he.getNumberOfExecutions() + " time";
688:                }
689:                return s;
690:            }
691:
692:            /**
693:             * Passing the focus request to the viewer's control.
694:             */
695:            public void setFocus() {
696:                viewer.getControl().setFocus();
697:            }
698:
699:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.