001: package visualdebugger.views;
002:
003: import java.net.URL;
004:
005: import org.eclipse.core.runtime.FileLocator;
006: import org.eclipse.core.runtime.IPath;
007: import org.eclipse.core.runtime.Path;
008: import org.eclipse.core.runtime.Platform;
009: import org.eclipse.jface.action.*;
010: import org.eclipse.jface.dialogs.MessageDialog;
011: import org.eclipse.jface.resource.ImageDescriptor;
012: import org.eclipse.jface.viewers.*;
013: import org.eclipse.swt.SWT;
014: import org.eclipse.swt.graphics.Image;
015: import org.eclipse.swt.layout.GridData;
016: import org.eclipse.swt.layout.GridLayout;
017: import org.eclipse.swt.widgets.*;
018: import org.eclipse.ui.IActionBars;
019: import org.eclipse.ui.IWorkbenchActionConstants;
020: import org.eclipse.ui.part.ViewPart;
021: import org.osgi.framework.Bundle;
022:
023: import visualdebugger.actions.StartVisualDebuggerAction;
024: import de.uka.ilkd.key.gui.Main;
025: import de.uka.ilkd.key.visualdebugger.DebuggerEvent;
026: import de.uka.ilkd.key.visualdebugger.DebuggerListener;
027: import de.uka.ilkd.key.visualdebugger.VisualDebugger;
028: import de.uka.ilkd.key.visualdebugger.executiontree.ETNode;
029: import de.uka.ilkd.key.visualdebugger.executiontree.ITNode;
030:
031: public class VisualDebuggerView extends ViewPart implements
032: DebuggerListener {
033: private TableViewer viewer;
034:
035: private Action runAction;
036:
037: private Action stepIntoAction;
038:
039: private Action stepOverAction;
040:
041: private Action doubleClickAction;
042:
043: private Action visualizeStateAction;
044:
045: private VisualDebugger vd = VisualDebugger.getVisualDebugger();
046:
047: private Shell shell;
048:
049: private StatusLineManager statusMgr;
050:
051: private String projectName;
052:
053: private Action showMainWindowAction;
054:
055: private Action allInvariants;
056:
057: private Action showImpliciteAttributes;
058:
059: private Action invariantsToPost;
060:
061: private Action quanSplitAction;
062:
063: /*
064: * The content provider class is responsible for providing objects to the
065: * view. It can wrap existing objects in adapters or simply return objects
066: * as-is. These objects may be sensitive to the current input of the view,
067: * or ignore it and always show the same content (like Task List, for
068: * example).
069: */
070:
071: class ViewContentProvider implements IStructuredContentProvider {
072: public void inputChanged(Viewer v, Object oldInput,
073: Object newInput) {
074: }
075:
076: public void dispose() {
077: }
078:
079: public Object[] getElements(Object parent) {
080: if (parent == null)
081: return new String[0];
082: else if (parent instanceof ETNode) {
083: ETNode n = (ETNode) parent;
084: return (ITNode[]) n.getITNodesArray();
085: } else if (parent instanceof ITNode[]) {
086: return (ITNode[]) parent;
087:
088: }
089:
090: return new String[] { "One", "Two", "Three" };
091: }
092: }
093:
094: class ViewLabelProvider extends LabelProvider implements
095: ITableLabelProvider {
096: public String getColumnText(Object obj, int index) {
097: if (obj instanceof ITNode) {
098: return vd.prettyPrint(((ITNode) obj).getPc());
099: }
100: return "";
101: }
102:
103: public Image getColumnImage(Object obj, int index) {
104: return getImage(obj);
105: }
106:
107: public Image getImage(Object obj) {
108: return null;
109: }
110: }
111:
112: class NameSorter extends ViewerSorter {
113: }
114:
115: /**
116: * The constructor.
117: */
118: public VisualDebuggerView() {
119: VisualDebugger.getVisualDebugger().addListener(this );
120: }
121:
122: /**
123: * This is a callback that will allow us to create the viewer and initialize
124: * it.
125: */
126: public void createPartControl(Composite parent) {
127: shell = parent.getShell();
128: GridLayout layout = new GridLayout();
129:
130: parent.setLayout(layout);
131: GridData data = new GridData(GridData.FILL_BOTH);
132: Label l = new Label(parent, SWT.BORDER);
133: l.setText("Path Condition:");
134:
135: l
136: .setToolTipText("Shows the path condition for the current selected node in the execution tree");
137: l.setLayoutData(new GridData(GridData.FILL_HORIZONTAL));
138:
139: viewer = new TableViewer(parent, SWT.MULTI | SWT.H_SCROLL
140: | SWT.V_SCROLL);
141:
142: viewer.getControl().setLayoutData(data);
143:
144: viewer.setContentProvider(new ViewContentProvider());
145: viewer.setLabelProvider(new ViewLabelProvider());
146: viewer.setSorter(new NameSorter());
147: // viewer.setInput(getViewSite()); //TODO ??
148:
149: // StatusLineManager m = new StatusLineManager();
150:
151: // this.getViewSite().;
152: // this.getConfigurationElement().
153:
154: // this.getViewSite().getActionBars().getStatusLineManager().setMessage("asdfasdf");
155: // StatusLineManager m = new StatusLineManager();
156: // m.createControl(viewer.getControl().getParent());
157: // m.setMessage("afasdfasdf");
158:
159: // SubStatusLineManager
160: // statusLineManager=(SubStatusLineManager)(getViewSite().getActionBars().getStatusLineManager());
161: // statusLineManager.setVisible(true);
162: // statusLineManager.setMessage("I'm read !");
163:
164: // GridData gid = new GridData();
165: // gid.horizontalAlignment = GridData.FILL;
166: // gid.verticalAlignment = GridData.BEGINNING;
167: // cmpTextEditor.setLayoutData(gid);
168:
169: statusMgr = new StatusLineManager();
170: statusMgr.createControl(parent, SWT.BORDER);
171: statusMgr.getControl().setLayoutData(
172: new GridData(GridData.FILL_HORIZONTAL));
173: statusMgr.setMessage("Ready");
174: // statusMgr.getProgressMonitor().beginTask("Test Task", 100);
175: // statusMgr.
176:
177: // Label lb=new Label((Composite)statusMgr.getControl(),SWT.NULL);
178: // gid = new GridData();
179: // gid.horizontalAlignment = GridData.FILL;
180: // gid.verticalAlignment = GridData.BEGINNING;
181: // statusMgr.getControl().setLayoutData(gid);
182: makeActions();
183: hookContextMenu();
184: hookDoubleClickAction();
185: contributeToActionBars();
186:
187: // getViewSite().getActionBars().getStatusLineManager().setMessage("adfasdfsa");
188: // getViewSite().getActionBars().getStatusLineManager().update(true);
189: // setStatus( "JFace Example v1.0" );
190: }
191:
192: private void hookContextMenu() {
193: MenuManager menuMgr = new MenuManager("#PopupMenu");
194: menuMgr.setRemoveAllWhenShown(true);
195: menuMgr.addMenuListener(new IMenuListener() {
196: public void menuAboutToShow(IMenuManager manager) {
197: VisualDebuggerView.this .fillContextMenu(manager);
198: }
199: });
200: Menu menu = menuMgr.createContextMenu(viewer.getControl());
201:
202: viewer.getControl().setMenu(menu);
203: getSite().registerContextMenu(menuMgr, viewer);
204: }
205:
206: private void setStatusMessage(final String message) {
207: Display display = shell.getDisplay();
208: final Thread barThread = new Thread("PBarThread") {
209: public void run() {
210: statusMgr.setMessage(message);
211: }
212: };
213: display.asyncExec(barThread);
214:
215: }
216:
217: private void contributeToActionBars() {
218: IActionBars bars = getViewSite().getActionBars();
219: fillLocalPullDown(bars.getMenuManager());
220: fillLocalToolBar(bars.getToolBarManager());
221: }
222:
223: private void fillLocalPullDown(IMenuManager manager) {
224: // Main.getInstance().isV
225: // manager.add(this.invariantsToPost);
226: manager.add(this .quanSplitAction);
227: manager.add(this .allInvariants);
228: manager.add(this .showImpliciteAttributes);
229: manager.add(new Separator());
230: manager.add(showMainWindowAction);
231:
232: // manager.add(stepIntoAction);
233: }
234:
235: private void fillContextMenu(IMenuManager manager) {
236: manager.add(visualizeStateAction);
237: // manager.add(stepIntoAction);
238: // // Other plug-ins can contribute there actions here
239: manager.add(new Separator(
240: IWorkbenchActionConstants.MB_ADDITIONS));
241: }
242:
243: private void fillLocalToolBar(IToolBarManager manager) {
244: manager.add(runAction);
245: manager.add(stepIntoAction);
246: manager.add(stepOverAction);
247: // manager.add(this.removeRed); TODO
248: // manager.add(testCaseAction);
249: }
250:
251: private void makeActions() {
252: runAction = new Action() {
253: public void run() {
254: vd.run();
255: // Goal g = ip.getProof().
256: // goal/Ruleappindex/clear,fill caches..
257:
258: // showMessage("Action 1 executed");
259: }
260: };
261: runAction.setText("Run");
262: runAction.setToolTipText("Run " + vd.getRunLimit()
263: + " statements");
264: runAction.setImageDescriptor(getImageDescriptor("run_exc.gif"));
265:
266: stepIntoAction = new Action() {
267: public void run() {
268: vd.stepInto();
269: // showMessage("Step Into");
270: }
271: };
272: stepIntoAction.setText("Step Into");
273: stepIntoAction.setToolTipText("Step Into");
274: stepIntoAction
275: .setImageDescriptor(getImageDescriptor("stepinto_co.gif"));
276:
277: stepOverAction = new Action() {
278: public void run() {
279: vd.stepOver();
280: }
281: };
282: stepOverAction.setText("Step Over");
283: stepOverAction.setToolTipText("Step Over");
284: stepOverAction
285: .setImageDescriptor(getImageDescriptor("stepover_co.gif"));
286:
287: showMainWindowAction = new Action("KeY-Prover Window",
288: Action.AS_CHECK_BOX) {
289: public void run() {
290: if (this .isChecked()) {
291: Main.getInstance().setVisible(true);
292: // Main.getInstance().toFront();
293: } else
294: Main.getInstance().setVisible(false);
295: VisualDebugger.showMainWindow = this .isChecked();
296:
297: }
298: };
299: showMainWindowAction.setChecked(false);
300: // showMainWindowAction.setText("KeY-Prover");
301: showMainWindowAction
302: .setToolTipText("Shows the KeY-Prover which runs in the background");
303:
304: quanSplitAction = new Action(
305: "Quantifier Instantiation with Splitting ",
306: Action.AS_CHECK_BOX) {
307: public void run() {
308: VisualDebugger.quan_splitting = this .isChecked();
309:
310: }
311: };
312: quanSplitAction.setChecked(false);
313: // showMainWindowAction.setText("KeY-Prover");
314: // quanSplitAction.setToolTipText("Shows the KeY-Prover which runs in
315: // the background");
316:
317: this .allInvariants = new Action("Use all Invariants",
318: Action.AS_CHECK_BOX) {
319: public void run() {
320: StartVisualDebuggerAction.allInvariants = allInvariants
321: .isChecked();
322:
323: }
324: };
325: allInvariants.setChecked(false);
326: // allInvariants.setText("KeY-Prover");
327: allInvariants
328: .setToolTipText("Adds all class invariants to the precondition");
329:
330: this .showImpliciteAttributes = new Action(
331: "Show Implicite Attributes", Action.AS_CHECK_BOX) {
332: public void run() {
333: VisualDebugger.showImpliciteAttr = showImpliciteAttributes
334: .isChecked();
335:
336: }
337: };
338: showImpliciteAttributes.setChecked(false);
339: visualizeStateAction = new Action() {
340: public void run() {
341: ISelection selection = viewer.getSelection();
342: Object obj = ((IStructuredSelection) selection)
343: .getFirstElement();
344: if (obj instanceof ITNode) {
345: vd.visualize((ITNode) obj);
346: }
347: }
348: };
349: visualizeStateAction.setText("Visualize State");
350:
351: doubleClickAction = new Action() {
352: public void run() {
353: ISelection selection = viewer.getSelection();
354: Object obj = ((IStructuredSelection) selection)
355: .getFirstElement();
356:
357: // vd.visualize(null);
358: if (obj instanceof ITNode) {
359:
360: vd.getMediator().getSelectionModel()
361: .setSelectedNode(((ITNode) obj).getNode());
362: }
363: // showMessage("Double-click detected on "+obj.toString());
364: }
365: };
366: }
367:
368: public void setInputThreadSave(final Object input) {
369: Display display = shell.getDisplay();
370: final Thread barThread = new Thread("PBarThread") {
371: public void run() {
372: viewer.setInput(input);
373: }
374: };
375: display.asyncExec(barThread);
376: }
377:
378: private void hookDoubleClickAction() {
379: viewer.addDoubleClickListener(new IDoubleClickListener() {
380: public void doubleClick(DoubleClickEvent event) {
381:
382: doubleClickAction.run();
383: }
384: });
385: }
386:
387: private void showMessage(String message) {
388: MessageDialog.openInformation(viewer.getControl().getShell(),
389: "Visual Debugger", message);
390: }
391:
392: protected StatusLineManager createStatusLineManager() {
393: StatusLineManager slm = new StatusLineManager();
394: slm.setMessage("TODO STATUSLINE!");
395: slm.setErrorMessage("message");
396: // slm.
397:
398: return slm;
399: }
400:
401: public synchronized void update(DebuggerEvent event) {
402: if (event.getType() == DebuggerEvent.PROJECT_LOADED_SUCCESSFUL) {
403: this .projectName = (String) event.getSubject();
404: setStatusMessage(projectName);
405: this .setInputThreadSave(null);
406: } else if (event.getType() == DebuggerEvent.EXEC_FINISHED) {
407: setStatusMessage(projectName);
408: } else if (event.getType() == DebuggerEvent.EXEC_STARTED) {
409: setStatusMessage(projectName + ": Running...");
410: } else
411:
412: if (event.getType() == DebuggerEvent.NODE_SELECTED) {
413: setInputThreadSave(event.getSubject());
414: ETNode ll = (ETNode) event.getSubject();
415:
416: // vd.removeRedundandPC(ll.getITNodes());
417: } else if (event.getType() == DebuggerEvent.RED_PC_REMOVED) {
418: setInputThreadSave(event.getSubject());
419: }
420: }
421:
422: /**
423: * Passing the focus request to the viewer's control.
424: */
425: public void setFocus() {
426: viewer.getControl().setFocus();
427: }
428:
429: private ImageDescriptor getImageDescriptor(String file) {
430: ImageDescriptor image = null;
431: try {
432: String filename = "icons/" + file;
433: Bundle bun = Platform.getBundle("VisualDebugger");
434: IPath ip = new Path(filename);
435: URL url = FileLocator.find(bun, ip, null);
436:
437: URL resolved = FileLocator.resolve(url);
438:
439: image = ImageDescriptor.createFromURL(resolved);
440: } catch (Exception e) {
441: e.printStackTrace();
442: }
443:
444: return image;
445: }
446:
447: }
|