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: package de.uka.ilkd.key.gui;
009:
010: import java.awt.Color;
011: import java.awt.Component;
012: import java.awt.Dimension;
013: import java.awt.FlowLayout;
014: import java.awt.event.*;
015: import java.util.ArrayList;
016:
017: import javax.swing.*;
018: import javax.swing.event.ListSelectionEvent;
019: import javax.swing.event.ListSelectionListener;
020: import javax.swing.event.TreeModelListener;
021: import javax.swing.table.AbstractTableModel;
022: import javax.swing.tree.DefaultTreeCellRenderer;
023: import javax.swing.tree.TreeCellRenderer;
024: import javax.swing.tree.TreeModel;
025: import javax.swing.tree.TreePath;
026:
027: import de.uka.ilkd.key.java.statement.LoopStatement;
028: import de.uka.ilkd.key.visualization.*;
029:
030: /*
031: * Created on 24.06.2005
032: */
033:
034: public class ProofVisTreeView extends JFrame implements
035: java.io.Serializable {
036:
037: private JPanel jContentPane = null;
038:
039: private JScrollPane jScrollPane = null;
040:
041: private JTree jTree = null;
042:
043: private JButton jButton = null;
044:
045: private JCheckBox jCheckBox = null;
046:
047: private JTable table;
048:
049: private ExecutionTraceModel[] traces, filterTraces;
050:
051: ExecutionTraceModel selection = null;
052:
053: public ProofVisTreeView(VisualizationModel visModel) {
054: this .traces = visModel.getExecutionTraces();
055: this .filterTraces = visModel.getInterestingExecutionTraces();
056: if (traces != null && traces.length > 0) {
057: selection = traces[0];
058: }
059:
060: setContentPane(getJContentPane());
061: setSize(425, 570);
062: setTitle("Visualization of Node "
063: + visModel.getNode().serialNr());
064: setVisible(true);
065: toFront();
066: }
067:
068: private String removeLineBreaks(String s) {
069: return s.replaceAll("\n", " ");
070: }
071:
072: /**
073: * This method initializes jContentPane
074: *
075: * @return javax.swing.JPanel
076: */
077: private JPanel getJContentPane() {
078: if (jContentPane == null) {
079: jContentPane = new JPanel();
080: jContentPane.setLayout(new FlowLayout());
081: jContentPane.add(getJScrollPane());
082: jContentPane.add(getSelectionPane());
083: jContentPane.add(getButtonPanel());
084: pack();
085: }
086:
087: return jContentPane;
088: }
089:
090: /**
091: * This method initializes jScrollPane
092: *
093: * @return javax.swing.JScrollPane
094: */
095: private JScrollPane getJScrollPane() {
096: if (jScrollPane == null) {
097:
098: jScrollPane = new JScrollPane(getJTree(),
099: JScrollPane.VERTICAL_SCROLLBAR_AS_NEEDED,
100: JScrollPane.HORIZONTAL_SCROLLBAR_AS_NEEDED);
101: jScrollPane
102: .setMinimumSize(new java.awt.Dimension(390, 400));
103: jScrollPane.setPreferredSize(new java.awt.Dimension(390,
104: 400));
105: }
106: return jScrollPane;
107: }
108:
109: /**
110: * This method initializes jTree
111: *
112: * @return javax.swing.JTree
113: */
114: private JTree getJTree() {
115: if (jTree == null) {
116: jTree = new JTree(new Object[0]);
117: ContextTraceElement cte = null;
118: if (selection != null) {
119: cte = selection.getFirstContextTraceElement();
120: jTree.setModel(new PVTreeModel(cte));
121: jTree.setCellRenderer(new CellRenderer());
122: }
123: jTree.setRootVisible(false);
124: ToolTipManager.sharedInstance().registerComponent(jTree);
125: MouseListener ml = new MouseAdapter() {
126: public void mousePressed(MouseEvent e) {
127: if (e.isPopupTrigger()) {
128: TreePath selPath = jTree.getPathForLocation(e
129: .getX(), e.getY());
130: if (selPath != null) {
131: JPopupMenu popup = new TreePopupMenu(
132: selPath.getLastPathComponent());
133: popup.show(e.getComponent(), e.getX(), e
134: .getY());
135: }
136: }
137: }
138: };
139: jTree.addMouseListener(ml);
140: if (cte != null && cte != TraceElement.END)
141: jTree.makeVisible(getPath());
142: }
143: return jTree;
144: }
145:
146: public TreePath getPath() {
147:
148: ContextTraceElement[] path = selection.getPath(selection
149: .getLastContextTraceElement());
150: ContextTraceElement[] pathResult = new ContextTraceElement[1 + path.length];
151: pathResult[0] = (ContextTraceElement) jTree.getModel()
152: .getRoot();
153: for (int i = 0; i < path.length; i++) {
154: pathResult[i + 1] = path[i];
155:
156: }
157:
158: return new TreePath(pathResult);
159: }
160:
161: /**
162: * This method initializes the button panel
163: *
164: * @return javax.swing.JButton
165: */
166: private JPanel getButtonPanel() {
167: JPanel buttonPanel = new JPanel();
168: if (jButton == null) {
169: jButton = new JButton();
170: jButton.setText("OK");
171: jButton.setPreferredSize(new java.awt.Dimension(75, 35));
172: }
173: ActionListener okListener = new ActionListener() {
174: public void actionPerformed(ActionEvent e) {
175: setVisible(false);
176: dispose();
177: }
178: };
179: jButton.addActionListener(okListener);
180:
181: if (jCheckBox == null) {
182: jCheckBox = new JCheckBox();
183: jCheckBox.setText("Filter uninteresting traces");
184: }
185: ItemListener itemListener = new ItemListener() {
186: public void itemStateChanged(ItemEvent e) {
187: Object source = e.getItemSelectable();
188: if (source == jCheckBox) {
189: if (e.getStateChange() == ItemEvent.SELECTED) {
190: ((TracesTableModel) table.getModel())
191: .setTraces(filterTraces);
192:
193: } else {
194: ((TracesTableModel) table.getModel())
195: .setTraces(traces);
196: }
197: table.repaint();
198: table.doLayout();
199: }
200: }
201: };
202: jButton.addActionListener(okListener);
203: jCheckBox.addItemListener(itemListener);
204: buttonPanel.add(jButton);
205: buttonPanel.add(jCheckBox);
206: return buttonPanel;
207: }
208:
209: public JScrollPane getSelectionPane() {
210: if (traces != null)
211: table = new JTable(new TracesTableModel(traces));
212: else
213: table = new JTable(0, 0);
214:
215: table
216: .setPreferredScrollableViewportSize(new Dimension(390,
217: 70));
218:
219: table.setSelectionMode(ListSelectionModel.SINGLE_SELECTION);
220:
221: ListSelectionModel rowSM = table.getSelectionModel();
222: if (selection != null)
223: table.addRowSelectionInterval(0, 0);
224: rowSM.addListSelectionListener(new ListSelectionListener() {
225: public void valueChanged(ListSelectionEvent e) {
226: // Ignore extra messages.
227: if (e.getValueIsAdjusting())
228: return;
229: ListSelectionModel lsm = (ListSelectionModel) e
230: .getSource();
231: if (lsm.isSelectionEmpty()) {
232: } else {
233: int selectedRow = lsm.getMinSelectionIndex();
234: selection = ((TracesTableModel) table.getModel())
235: .getTrace(selectedRow);
236: ContextTraceElement cte = selection
237: .getFirstContextTraceElement();
238: jTree.setModel(new PVTreeModel(cte));
239: if (cte != TraceElement.END)
240: jTree.makeVisible(getPath());
241: jTree.updateUI();
242: }
243: }
244: });
245: table.setColumnSelectionAllowed(false);
246: // Create the scroll pane and add the table to it.
247: JScrollPane scrollPane = new JScrollPane(table);
248: scrollPane.setPreferredSize(new Dimension(390, 70));
249: scrollPane.setMinimumSize(new Dimension(390, 70));
250: // Add the scroll pane to this panel.
251: return (scrollPane);
252:
253: }
254:
255: class PVTreeModel implements TreeModel {
256:
257: ParentContextTraceElement root = new ParentContextTraceElement();
258:
259: Object[] children;
260:
261: public PVTreeModel(ContextTraceElement ste) {
262: root = new ParentContextTraceElement();
263: ArrayList childr = new ArrayList();
264: ContextTraceElement cte = ste;
265: while ((cte != TraceElement.END)
266: && (TraceElement.PARENTROOT == cte.getParent())) {
267: childr.add(cte);
268: if (cte instanceof ParentContextTraceElement)
269: cte = ((ParentContextTraceElement) cte).stepOver();
270: else
271: cte = cte.getNextExecuted();
272: }
273: children = childr.toArray();
274: }
275:
276: public void addTreeModelListener(TreeModelListener l) {
277: }
278:
279: public Object getChild(Object parent, int index) {
280: if (parent == root) {
281: return children[index];
282: } else
283: return ((ParentContextTraceElement) parent)
284: .getChildren()[index];
285: }
286:
287: public int getChildCount(Object parent) {
288: if (parent == root)
289: return children.length;
290: else
291: return ((ParentContextTraceElement) parent)
292: .getChildren().length;
293: }
294:
295: public int getIndexOfChild(Object parent, Object child) {
296: if ((parent == null) || (child == null))
297: return -1;
298: Object[] ch = ((ParentContextTraceElement) parent)
299: .getChildren();
300: for (int i = 0; i < ch.length; i++) {
301: if (ch[i].equals(child))
302: return i;
303: }
304: return -1;
305: }
306:
307: public Object getRoot() {
308: return root;
309: }
310:
311: public boolean isLeaf(Object node) {
312: if (node == root)
313: return false;
314: if (!(node instanceof ParentContextTraceElement))
315: return true;
316: if (((ParentContextTraceElement) node).getChildren().length == 0)
317: return true;
318: return false;
319:
320: }
321:
322: public void removeTreeModelListener(TreeModelListener l) {
323: }
324:
325: public void valueForPathChanged(TreePath path, Object newValue) {
326: }
327:
328: }
329:
330: class CellRenderer extends DefaultTreeCellRenderer implements
331: TreeCellRenderer, java.io.Serializable {
332:
333: public Component getTreeCellRendererComponent(JTree list,
334: Object value, boolean selected, boolean expanded,
335: boolean leaf, int row, boolean hasFocus) {
336: String s;
337: ContextTraceElement cte = null;
338: if (value != null) {
339: cte = (ContextTraceElement) value;
340: if (cte.getContextStatement() != null) {
341: s = "" + cte.getContextStatement();
342: } else {
343: s = "" + cte.getSrcElement();
344: }
345:
346: int i = s.indexOf("\n");
347: if (i > -1) {
348: s = s.substring(0, i);
349: }
350: } else {
351: s = "NULL";
352: }
353: DefaultTreeCellRenderer tree_cell = (DefaultTreeCellRenderer) super
354: .getTreeCellRendererComponent(list, s, selected,
355: expanded, leaf, row, hasFocus);
356:
357: tree_cell.setBackground(Color.WHITE);
358: tree_cell.setBackgroundNonSelectionColor(Color.WHITE);
359: tree_cell.setBackgroundSelectionColor(Color.WHITE);
360:
361: tree_cell.setFont(list.getFont());
362: tree_cell.setText(s);
363:
364: if (cte != null) {
365: String toolTipText = "<html><b>Node " + cte.serialNr()
366: + "</b>";
367: if (cte.getLabel() != null
368: && (cte.getLabel().length() > 0)) {
369: toolTipText += "<br><b>" + cte.getLabel() + "</b>";
370: }
371: if (cte != TraceElement.PARENTROOT
372: && cte.getParent() != null
373: && (cte.getParent() != TraceElement.PARENTROOT)
374: && (cte.getParent().getSrcElement() instanceof LoopStatement)) {
375: toolTipText += "<br><b>Unwound:</b> "
376: + cte.getNumberOfExecutions() + " time";
377: if (cte.getNumberOfExecutions() > 1)
378: toolTipText += "s";
379: }
380: if ((cte == selection.getLastContextTraceElement())
381: && selection.uncaughtException()) {
382: tree_cell.setBackground(Color.PINK);
383: tree_cell
384: .setBackgroundNonSelectionColor(Color.PINK);
385: tree_cell.setBackgroundSelectionColor(Color.PINK);
386: toolTipText += "<br><b>Uncaught Exception: </b>"
387: + removeLineBreaks(""
388: + selection.getUncaughtException()
389: .getSrcElement());
390: }
391: toolTipText += "</html>";
392: tree_cell.setToolTipText(toolTipText);
393: }
394: tree_cell.setLeafIcon(null);
395: return tree_cell;
396: }
397:
398: }
399:
400: class TracesTableModel extends AbstractTableModel {
401: String[] columnNames = { "Java Program", "First Node",
402: "Last Node" };
403:
404: ExecutionTraceModel[] traces;
405:
406: public TracesTableModel(ExecutionTraceModel[] traces) {
407: super ();
408: this .traces = traces;
409:
410: }
411:
412: public int getColumnCount() {
413: return columnNames.length;
414: }
415:
416: public int getRowCount() {
417: return traces.length;
418: }
419:
420: public String getColumnName(int col) {
421: return columnNames[col];
422: }
423:
424: public Object getValueAt(int row, int col) {
425: if (col == 0)
426: return removeLineBreaks(""
427: + traces[row].getFirstTraceElement()
428: .getProgram());
429: else if (col == 1)
430: return "" + traces[row].getFirstNode().serialNr();
431: else
432: return "" + traces[row].getLastNode().serialNr();
433: }
434:
435: public Class getColumnClass(int c) {
436: return getValueAt(0, c).getClass();
437: }
438:
439: public boolean isCellEditable(int row, int col) {
440: return false;
441: }
442:
443: public ExecutionTraceModel getTrace(int row) {
444: return traces[row];
445: }
446:
447: public void setTraces(ExecutionTraceModel[] traces) {
448: this .traces = traces;
449: fireTableDataChanged();
450: }
451:
452: }
453:
454: class TreePopupMenu extends JPopupMenu implements ActionListener {
455:
456: private JMenuItem showNode = new JMenuItem("Show Node");
457: private ContextTraceElement cte;
458:
459: public TreePopupMenu(Object node) {
460: super ("Choose Action");
461: if (node instanceof ContextTraceElement) {
462: cte = (ContextTraceElement) node;
463: create();
464: }
465: }
466:
467: private void create() {
468: this .add(showNode);
469: showNode.addActionListener(this );
470: }
471:
472: public void actionPerformed(ActionEvent e) {
473: if (e.getSource() == showNode) {
474: Main.getInstance().mediator().getSelectionModel()
475: .setSelectedNode(cte.node());
476: }
477: }
478: }
479:
480: }
|