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: package de.uka.ilkd.key.gui;
010:
011: import java.awt.*;
012: import java.awt.event.ActionEvent;
013: import java.awt.event.ActionListener;
014: import java.util.*;
015:
016: import javax.swing.*;
017: import javax.swing.border.TitledBorder;
018: import javax.swing.event.ListSelectionEvent;
019: import javax.swing.event.ListSelectionListener;
020: import javax.swing.event.TreeSelectionEvent;
021: import javax.swing.event.TreeSelectionListener;
022: import javax.swing.tree.DefaultMutableTreeNode;
023: import javax.swing.tree.DefaultTreeCellRenderer;
024: import javax.swing.tree.DefaultTreeModel;
025: import javax.swing.tree.TreePath;
026:
027: import de.uka.ilkd.key.casetool.ModelClass;
028: import de.uka.ilkd.key.speclang.*;
029: import de.uka.ilkd.key.util.Debug;
030:
031: /**
032: * A dialog for selecting class invariants.
033: */
034: public class ClassInvariantSelectionPanel extends JPanel {
035:
036: private Set modelClasses;
037: private boolean useThroughoutInvs;
038:
039: private ListOfClassInvariant selectedInvs = SLListOfClassInvariant.EMPTY_LIST;
040: private JTree classTree;
041: private JList invList;
042: private ModelClass selectedClass = null;
043: private JPanel rightButtonPanel;
044: private java.util.List selectionListeners = new LinkedList();
045:
046: /**
047: * Creates and displays a dialog box asking the user to select a set of
048: * invariants.
049: * @param modelClasses the classes to choose invariants from
050: */
051: public ClassInvariantSelectionPanel(Set modelClasses,
052: boolean useThroughoutInvs, ModelClass defaultClass,
053: boolean selectDefaultInvs) {
054:
055: this .modelClasses = modelClasses;
056: this .useThroughoutInvs = useThroughoutInvs;
057:
058: //create class tree
059: classTree = buildClassTree(modelClasses);
060: classTree.addTreeSelectionListener(new TreeSelectionListener() {
061: public void valueChanged(TreeSelectionEvent e) {
062: DefaultMutableTreeNode selectedNode = (DefaultMutableTreeNode) (e
063: .getPath().getLastPathComponent());
064: TreeEntry te = (TreeEntry) (selectedNode
065: .getUserObject());
066: Debug.assertTrue(!selectedNode.isLeaf()
067: || te.modelClass != null);
068: selectedClass = te.modelClass;
069: updateInvList();
070: }
071: });
072: classTree.setCellRenderer(new DefaultTreeCellRenderer() {
073: private final Color MEDIUMGREEN = new Color(80, 150, 0);
074: private final Color DARKGREEN = new Color(0, 120, 90);
075: private final Font BOLDFONT = ClassInvariantSelectionPanel.this
076: .getFont().deriveFont(Font.BOLD, 10);
077:
078: public Component getTreeCellRendererComponent(JTree tree,
079: Object value, boolean selected, boolean expanded,
080: boolean leaf, int row, boolean hasFocus) {
081: DefaultMutableTreeNode node = (DefaultMutableTreeNode) value;
082: TreeEntry te = (TreeEntry) (node.getUserObject());
083: if (te.numSelectedInvs == te.numInvs) {
084: setTextNonSelectionColor(MEDIUMGREEN);
085: setTextSelectionColor(MEDIUMGREEN);
086: } else if (te.numSelectedInvs > 0) {
087: setTextNonSelectionColor(DARKGREEN);
088: setTextSelectionColor(DARKGREEN);
089: } else {
090: setTextNonSelectionColor(Color.BLACK);
091: setTextSelectionColor(Color.BLACK);
092: }
093: setFont(BOLDFONT);
094: return super .getTreeCellRendererComponent(tree, value,
095: selected, expanded, leaf, row, hasFocus);
096: }
097: });
098:
099: //create inv list
100: invList = new JList();
101: invList
102: .setSelectionMode(ListSelectionModel.MULTIPLE_INTERVAL_SELECTION);
103: invList.addListSelectionListener(new ListSelectionListener() {
104: public void valueChanged(ListSelectionEvent e) {
105: if (e.getValueIsAdjusting()) {
106: return;
107: }
108:
109: ListModel model = invList.getModel();
110: int firstIndex = e.getFirstIndex();
111: int lastIndex = Math.min(e.getLastIndex(), model
112: .getSize() - 1);
113: for (int i = firstIndex; i <= lastIndex; i++) {
114: ClassInvariant inv = (ClassInvariant) (model
115: .getElementAt(i));
116: if (invList.isSelectedIndex(i)) {
117: addToSelection(inv);
118: } else {
119: removeFromSelection(inv);
120: }
121: }
122: fireSelectionChanged(e);
123: }
124: });
125:
126: //create list panel
127: JPanel listPanel = new JPanel();
128: listPanel.setLayout(new BoxLayout(listPanel, BoxLayout.X_AXIS));
129: add(listPanel);
130:
131: //create class scroll pane
132: JScrollPane classScrollPane = new JScrollPane(classTree);
133: classScrollPane.setBorder(new TitledBorder("Classes"));
134: Dimension classScrollPaneDim = new Dimension(220, 400);
135: classScrollPane.setPreferredSize(classScrollPaneDim);
136: classScrollPane.setMinimumSize(classScrollPaneDim);
137: listPanel.add(classScrollPane);
138:
139: //create invariant scroll pane
140: JScrollPane invScrollPane = new JScrollPane(invList);
141: invScrollPane.setBorder(new TitledBorder(
142: (useThroughoutInvs ? "Throughout invariants"
143: : "Invariants")));
144: Dimension invScrollPaneDim = new Dimension(440, 400);
145: invScrollPane.setPreferredSize(invScrollPaneDim);
146: invScrollPane.setMinimumSize(invScrollPaneDim);
147: listPanel.add(invScrollPane);
148:
149: //create button panel
150: JPanel buttonPanel = new JPanel();
151: buttonPanel.setLayout(new BoxLayout(buttonPanel,
152: BoxLayout.X_AXIS));
153: add(buttonPanel);
154: Dimension buttonDim = new Dimension(95, 25);
155:
156: //create left button panel
157: JPanel leftButtonPanel = new JPanel();
158: leftButtonPanel
159: .setLayout(new FlowLayout(FlowLayout.LEFT, 5, 5));
160: buttonPanel.add(leftButtonPanel);
161:
162: //create right button panel
163: rightButtonPanel = new JPanel();
164: rightButtonPanel.setLayout(new FlowLayout(FlowLayout.RIGHT, 5,
165: 5));
166: buttonPanel.add(rightButtonPanel);
167:
168: //create "select all" button
169: JButton selectButton = new JButton("Select all");
170: selectButton.setPreferredSize(buttonDim);
171: selectButton.setMinimumSize(buttonDim);
172: selectButton.addActionListener(new ActionListener() {
173: public void actionPerformed(ActionEvent e) {
174: selectAll();
175: updateInvList();
176: }
177: });
178: leftButtonPanel.add(selectButton);
179:
180: //create "unselect all" button
181: JButton unselectButton = new JButton("Unselect all");
182: unselectButton.setPreferredSize(buttonDim);
183: unselectButton.setMinimumSize(buttonDim);
184: unselectButton.addActionListener(new ActionListener() {
185: public void actionPerformed(ActionEvent e) {
186: unselectAll();
187: updateInvList();
188: }
189: });
190: leftButtonPanel.add(unselectButton);
191:
192: //set default selection
193: if (selectDefaultInvs) {
194: selectAllForClass(defaultClass);
195: }
196: openClassInTree(defaultClass);
197:
198: //show dialog
199: setLayout(new BoxLayout(this , BoxLayout.Y_AXIS));
200: }
201:
202: public JPanel getButtonPanel() {
203: return rightButtonPanel;
204: }
205:
206: public void addInvariantSelectionListener(
207: ListSelectionListener listener) {
208: selectionListeners.add(listener);
209: }
210:
211: private void fireSelectionChanged(ListSelectionEvent e) {
212: Iterator it = selectionListeners.iterator();
213: while (it.hasNext()) {
214: ((ListSelectionListener) it.next()).valueChanged(e);
215: }
216: }
217:
218: private ListOfClassInvariant getRelevantInvs(ModelClass modelClass) {
219: if (useThroughoutInvs) {
220: return modelClass.getMyThroughoutClassInvariants();
221: } else {
222: return modelClass.getMyClassInvariants();
223: }
224: }
225:
226: private DefaultMutableTreeNode getChildByString(
227: DefaultMutableTreeNode parentNode, String childString) {
228: int numChildren = parentNode.getChildCount();
229: for (int i = 0; i < numChildren; i++) {
230: DefaultMutableTreeNode childNode = (DefaultMutableTreeNode) (parentNode
231: .getChildAt(i));
232:
233: TreeEntry te = (TreeEntry) (childNode.getUserObject());
234: if (childString.equals(te.string)) {
235: return childNode;
236: }
237: }
238: return null;
239: }
240:
241: private void insertIntoClassTree(DefaultMutableTreeNode rootNode,
242: ModelClass modelClass) {
243: String fullClassName = modelClass.getFullClassName();
244: int length = fullClassName.length();
245: int index = -1;
246: DefaultMutableTreeNode node = rootNode;
247:
248: do {
249: //get next part of the name
250: int lastIndex = index;
251: index = fullClassName.indexOf(".", ++index);
252: if (index == -1) {
253: index = length;
254: }
255: String namePart = fullClassName.substring(lastIndex + 1,
256: index);
257:
258: //try to get child node; otherwise, create and insert it
259: DefaultMutableTreeNode childNode = getChildByString(node,
260: namePart);
261: if (childNode == null) {
262: TreeEntry te = new TreeEntry(namePart);
263: childNode = new DefaultMutableTreeNode(te);
264: node.add(childNode);
265: }
266:
267: //go down to child node
268: node = childNode;
269: } while (index != length);
270:
271: //save model class in leaf
272: TreeEntry te = (TreeEntry) (node.getUserObject());
273: te.modelClass = modelClass;
274: }
275:
276: private void setInvCounters(DefaultMutableTreeNode node) {
277: int numInvs = 0;
278:
279: int numChildren = node.getChildCount();
280: for (int i = 0; i < numChildren; i++) {
281: DefaultMutableTreeNode childNode = (DefaultMutableTreeNode) (node
282: .getChildAt(i));
283: setInvCounters(childNode);
284: TreeEntry te = (TreeEntry) (childNode.getUserObject());
285: numInvs += te.numInvs;
286: }
287:
288: TreeEntry te = (TreeEntry) (node.getUserObject());
289: if (te.modelClass != null) {
290: numInvs += getRelevantInvs(te.modelClass).size();
291: }
292:
293: te.numInvs = numInvs;
294: }
295:
296: private void setSelectedInvCounters(DefaultMutableTreeNode node) {
297: int numSelectedInvs = 0;
298:
299: int numChildren = node.getChildCount();
300: for (int i = 0; i < numChildren; i++) {
301: DefaultMutableTreeNode childNode = (DefaultMutableTreeNode) (node
302: .getChildAt(i));
303: setSelectedInvCounters(childNode);
304: TreeEntry te = (TreeEntry) (childNode.getUserObject());
305: numSelectedInvs += te.numSelectedInvs;
306: }
307:
308: TreeEntry te = (TreeEntry) (node.getUserObject());
309: if (te.modelClass != null) {
310: ListOfClassInvariant invs = getRelevantInvs(te.modelClass);
311: IteratorOfClassInvariant it = invs.iterator();
312: while (it.hasNext()) {
313: if (selectedInvs.contains(it.next())) {
314: numSelectedInvs++;
315: }
316: }
317: }
318:
319: te.numSelectedInvs = numSelectedInvs;
320: }
321:
322: private JTree buildClassTree(Set modelClasses) {
323: //sort classes alphabetically
324: Object[] mca = modelClasses.toArray();
325: Arrays.sort(mca, new Comparator() {
326: public int compare(Object o1, Object o2) {
327: ModelClass mc1 = (ModelClass) o1;
328: ModelClass mc2 = (ModelClass) o2;
329: return mc1.getFullClassName().compareTo(
330: mc2.getFullClassName());
331: }
332: });
333:
334: //build tree
335: TreeEntry rootEntry = new TreeEntry("");
336: DefaultMutableTreeNode rootNode = new DefaultMutableTreeNode(
337: rootEntry);
338: for (int i = 0; i < mca.length; i++) {
339: ModelClass modelClass = (ModelClass) (mca[i]);
340: if (getRelevantInvs(modelClass).size() > 0) {
341: insertIntoClassTree(rootNode, modelClass);
342: }
343: }
344:
345: //set inv counters
346: setInvCounters(rootNode);
347:
348: JTree result = new JTree(new DefaultTreeModel(rootNode));
349: //result.setRootVisible(false);
350: return result;
351: }
352:
353: private void addToSelection(ClassInvariant inv) {
354: //make sure inv is not selected already
355: if (selectedInvs.contains(inv)) {
356: return;
357: }
358:
359: //add it to the selection
360: selectedInvs = selectedInvs.prepend(inv);
361:
362: //update selection counters in tree
363: Object[] nodes = classTree.getSelectionPath().getPath();
364: for (int i = 0; i < nodes.length; i++) {
365: DefaultMutableTreeNode node = (DefaultMutableTreeNode) (nodes[i]);
366: TreeEntry te = (TreeEntry) (node.getUserObject());
367: te.numSelectedInvs++;
368: Debug.assertTrue(te.numSelectedInvs > 0
369: && te.numSelectedInvs <= te.numInvs);
370:
371: }
372: classTree.repaint();
373: }
374:
375: private void removeFromSelection(ClassInvariant inv) {
376: //make sure inv is currently selected
377: if (!selectedInvs.contains(inv)) {
378: return;
379: }
380:
381: //remove it from the selection
382: selectedInvs = selectedInvs.removeFirst(inv);
383:
384: //update selection counters in tree
385: Object[] nodes = classTree.getSelectionPath().getPath();
386: for (int i = 0; i < nodes.length; i++) {
387: DefaultMutableTreeNode node = (DefaultMutableTreeNode) (nodes[i]);
388: TreeEntry te = (TreeEntry) (node.getUserObject());
389: te.numSelectedInvs--;
390: Debug.assertTrue(te.numSelectedInvs >= 0
391: && te.numSelectedInvs < te.numInvs);
392: }
393: classTree.repaint();
394: }
395:
396: private void selectAllForClass(ModelClass modelClass) {
397: //select invariants of this class
398: selectedInvs = getRelevantInvs(modelClass);
399:
400: //update selection counters in tree
401: DefaultMutableTreeNode rootNode = (DefaultMutableTreeNode) (classTree
402: .getModel().getRoot());
403: setSelectedInvCounters(rootNode);
404: classTree.repaint();
405: }
406:
407: private void selectAll() {
408: //select all
409: selectedInvs = SLListOfClassInvariant.EMPTY_LIST;
410: Iterator it = modelClasses.iterator();
411: while (it.hasNext()) {
412: ModelClass modelClass = (ModelClass) (it.next());
413: selectedInvs = selectedInvs
414: .append(getRelevantInvs(modelClass));
415: }
416:
417: //update selection counters in tree
418: DefaultMutableTreeNode rootNode = (DefaultMutableTreeNode) (classTree
419: .getModel().getRoot());
420: setSelectedInvCounters(rootNode);
421: classTree.repaint();
422: }
423:
424: private void unselectAll() {
425: //unselect all
426: selectedInvs = SLListOfClassInvariant.EMPTY_LIST;
427:
428: //update selection counters in tree
429: DefaultMutableTreeNode rootNode = (DefaultMutableTreeNode) (classTree
430: .getModel().getRoot());
431: setSelectedInvCounters(rootNode);
432: classTree.repaint();
433: }
434:
435: private void updateInvList() {
436: invList.setValueIsAdjusting(true);
437:
438: if (selectedClass == null) {
439: invList.setListData(new Object[0]);
440: } else {
441: ListOfClassInvariant invariants = getRelevantInvs(selectedClass);
442: invList.setListData(invariants.toArray());
443:
444: IteratorOfClassInvariant it = selectedInvs.iterator();
445: while (it.hasNext()) {
446: invList.setSelectedValue(it.next(), false);
447: }
448: }
449:
450: invList.setValueIsAdjusting(false);
451: }
452:
453: private boolean openClassInTree(ModelClass modelClass) {
454: //get tree path
455: Vector pathVector = new Vector();
456:
457: String fullClassName = modelClass.getFullClassName();
458: int length = fullClassName.length();
459: int index = -1;
460: DefaultMutableTreeNode node = (DefaultMutableTreeNode) (classTree
461: .getModel().getRoot());
462: Debug.assertTrue(node != null);
463: do {
464: //save current node
465: pathVector.add(node);
466:
467: //get next part of the name
468: int lastIndex = index;
469: index = fullClassName.indexOf(".", ++index);
470: if (index == -1) {
471: index = length;
472: }
473: String namePart = fullClassName.substring(lastIndex + 1,
474: index);
475:
476: //get child node, go down to it
477: DefaultMutableTreeNode childNode = getChildByString(node,
478: namePart);
479: if (childNode == null) {
480: return false;
481: }
482: node = childNode;
483: } while (index != length);
484: TreePath incompletePath = new TreePath(pathVector.toArray());
485:
486: TreePath path = incompletePath.pathByAddingChild(node);
487:
488: classTree.expandPath(incompletePath);
489: classTree.setSelectionRow(classTree.getRowForPath(path));
490: return true;
491: }
492:
493: /**
494: * Returns the selected set of invariants.
495: */
496: public ListOfClassInvariant getClassInvariants() {
497: return selectedInvs;
498: }
499:
500: public JList getInvList() {
501: return invList;
502: }
503:
504: private static class TreeEntry {
505: public String string;
506: public ModelClass modelClass = null;
507: public int numInvs = 0;
508: public int numSelectedInvs = 0;
509:
510: public TreeEntry(String string) {
511: this .string = string;
512: }
513:
514: public String toString() {
515: return string;
516: }
517: }
518: }
|