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;
012:
013: import java.awt.Color;
014: import java.awt.Component;
015: import java.awt.Font;
016: import java.awt.event.MouseAdapter;
017: import java.awt.event.MouseEvent;
018: import java.awt.event.MouseListener;
019: import java.util.ArrayList;
020: import java.util.List;
021: import java.util.WeakHashMap;
022:
023: import javax.swing.*;
024: import javax.swing.event.ListDataEvent;
025: import javax.swing.event.ListDataListener;
026:
027: import de.uka.ilkd.key.gui.configuration.Config;
028: import de.uka.ilkd.key.logic.Sequent;
029: import de.uka.ilkd.key.pp.LogicPrinter;
030: import de.uka.ilkd.key.pp.ProgramPrinter;
031: import de.uka.ilkd.key.proof.*;
032: import de.uka.ilkd.key.util.Debug;
033:
034: public class GoalList extends JList {
035:
036: private static final ImageIcon keyIcon = IconFactory
037: .keyHole(20, 20);
038:
039: private KeYMediator mediator;
040:
041: /** the model used by this view */
042: private final SelectingGoalListModel selectingListModel;
043: private final GoalListModel goalListModel;
044:
045: /** interactive prover listener */
046: private GoalListInteractiveListener interactiveListener;
047:
048: /** KeYSelection-Listener */
049: private GoalListSelectionListener selectionListener;
050:
051: /** listens to gui events */
052: private GoalListGUIListener guiListener;
053:
054: private MouseListener mouseListener = new GoalListMouseListener();
055:
056: private class GoalListMouseListener extends MouseAdapter implements
057: java.io.Serializable {
058: public void mouseClicked(MouseEvent e) {
059: if (e.getClickCount() == 1) {
060: goalChosen();
061: }
062: }
063: }
064:
065: public GoalList(KeYMediator mediator) {
066: interactiveListener = new GoalListInteractiveListener();
067: selectionListener = new GoalListSelectionListener();
068: guiListener = new GoalListGUIListener();
069:
070: setSelectionMode(ListSelectionModel.SINGLE_SELECTION);
071: setMediator(mediator);
072: goalListModel = new GoalListModel();
073: selectingListModel = new SelectingGoalListModel(goalListModel);
074: selectingListModel.setProof(mediator.getSelectedProof());
075: setModel(selectingListModel);
076: setCellRenderer(new IconCellRenderer());
077: addMouseListener(mouseListener);
078: updateUI();
079: }
080:
081: /** set the KeYMediator */
082: private void setMediator(KeYMediator m) {
083: if (mediator != null) {
084: unregister();
085: }
086: mediator = m;
087: register();
088: }
089:
090: public void updateUI() {
091: super .updateUI();
092: Font myFont = UIManager.getFont(Config.KEY_FONT_GOAL_LIST_VIEW);
093: if (myFont != null) {
094: setFont(myFont);
095: } else {
096: Debug
097: .out(
098: "goallist: Warning: Use standard font. Could not find font:",
099: Config.KEY_FONT_GOAL_LIST_VIEW);
100: }
101: }
102:
103: private void register() {
104: mediator().addKeYSelectionListener(selectionListener);
105: mediator().addAutoModeListener(interactiveListener);
106: mediator().addGUIListener(guiListener);
107: }
108:
109: private void unregister() {
110: mediator().removeKeYSelectionListener(selectionListener);
111: mediator().removeAutoModeListener(interactiveListener);
112: mediator().removeGUIListener(guiListener);
113: }
114:
115: public void removeNotify() { // not used?
116: unregister();
117: super .removeNotify();
118: }
119:
120: private KeYMediator mediator() {
121: return mediator;
122: }
123:
124: private void goalChosen() {
125: Goal goal = (Goal) getSelectedValue();
126: if (goal != null) {
127: mediator().goalChosen(goal);
128: }
129: }
130:
131: /** overrides setVisible from JFrame
132: * takes care that the view item is in the right state
133: */
134: public void setVisible(boolean b) { // ???
135: super .setVisible(b);
136: }
137:
138: private void selectSelectedGoal() {
139: // otherwise it can happen that after removing list entries a wrong row
140: // is selected
141: clearSelection();
142:
143: if (mediator() != null) {
144: try {
145: final Goal selGoal = mediator().getSelectedGoal();
146: if (selGoal != null)
147: setSelectedValue(selGoal, true);
148: } catch (IllegalStateException e) {
149: // this exception occurs if no proof is loaded
150: // do nothing
151: Debug.out("GoalList: No proof loaded.");
152: }
153: }
154:
155: validate();
156: }
157:
158: private class GoalListGUIListener implements GUIListener,
159: java.io.Serializable {
160: /** invoked if a frame that wants modal access is opened */
161: public void modalDialogOpened(GUIEvent e) {
162: setEnabled(false);
163: }
164:
165: /** invoked if a frame that wants modal access is closed */
166: public void modalDialogClosed(GUIEvent e) {
167: setEnabled(true);
168: }
169:
170: public void shutDown(GUIEvent e) {
171: }
172:
173: }
174:
175: private class GoalListSelectionListener implements
176: KeYSelectionListener {
177:
178: /** focused node has changed */
179: public void selectedNodeChanged(KeYSelectionEvent e) {
180: selectSelectedGoal();
181: }
182:
183: /** the selected proof has changed (e.g. a new proof has been
184: * loaded) */
185: public void selectedProofChanged(KeYSelectionEvent e) {
186: Debug.out("GoalList: initialize with new proof");
187: selectingListModel.setProof(e.getSource()
188: .getSelectedProof());
189: validate();
190: }
191: }
192:
193: private class GoalListInteractiveListener implements
194: AutoModeListener {
195:
196: /** invoked if automatic executiion of heuristics has started
197: */
198: public void autoModeStarted(ProofEvent e) {
199: if (goalListModel.isAttentive()) {
200: mediator()
201: .removeKeYSelectionListener(selectionListener);
202: }
203: goalListModel.setAttentive(false);
204: }
205:
206: /** invoked if automatic execution of heuristics has stopped
207: */
208: public void autoModeStopped(ProofEvent e) {
209: if (!goalListModel.isAttentive()) {
210: mediator().addKeYSelectionListener(selectionListener);
211: }
212: goalListModel.setAttentive(true);
213: }
214:
215: }
216:
217: private static class GoalListModel extends AbstractListModel {
218:
219: /** the proof the model belongs to */
220: private Proof proof;
221: /** */
222: private List goals;
223: /** is used to indicate if the model has to be updated */
224: private boolean attentive;
225: /** listens to the proof */
226: private final ProofTreeListener proofTreeListener = new GoalListProofTreeListener();
227:
228: GoalListModel() {
229: goals = new ArrayList(10);
230: }
231:
232: /**
233: * the proof this view belongs to has changed
234: */
235: private void setProof(Proof p) {
236: clear();
237: if (proof != null) {
238: proof.removeProofTreeListener(proofTreeListener);
239: }
240: proof = p;
241: if (proof != null) {
242: proof.addProofTreeListener(proofTreeListener);
243: add(proof.openGoals());
244: }
245: attentive = true;
246: }
247:
248: /** Sets whether this object should respond to changes in the
249: * the proof immediately. */
250: private void setAttentive(boolean b) {
251: if ((b != attentive) && (proof != null)) {
252: if (b) {
253: proof.addProofTreeListener(proofTreeListener);
254: clear();
255: add(proof.openGoals());
256: } else {
257: proof.removeProofTreeListener(proofTreeListener);
258: }
259: }
260: attentive = b;
261: }
262:
263: /** returns true if the model respond to changes in the proof
264: * immediately */
265: public boolean isAttentive() {
266: return attentive;
267: }
268:
269: public void add(ListOfGoal g) {
270: if (g != SLListOfGoal.EMPTY_LIST) {
271: final IteratorOfGoal it = g.iterator();
272: while (it.hasNext()) {
273: goals.add(it.next());
274: }
275: fireIntervalAdded(this , goals.size() - g.size(), goals
276: .size() - 1);
277: }
278: }
279:
280: public void add(Goal g) {
281: if (g != null) {
282: goals.add(g);
283: int index = goals.indexOf(g);
284: fireIntervalAdded(this , index, index);
285: }
286: }
287:
288: public void remove(Goal g) {
289: int index = goals.indexOf(g);
290: if (index > -1) {
291: goals.remove(g);
292: fireIntervalRemoved(this , index, index);
293: }
294: }
295:
296: public void clear() {
297: int size = goals.size();
298: if (size > 0) {
299: goals.clear();
300: fireIntervalRemoved(this , 0, size - 1);
301: }
302: }
303:
304: public int getSize() {
305: return goals.size();
306: }
307:
308: public Object getElementAt(int i) {
309: return goals.get(i);
310: }
311:
312: class GoalListProofTreeListener implements ProofTreeListener,
313: java.io.Serializable {
314:
315: /*
316: * (non-Javadoc)
317: *
318: * @see de.uka.ilkd.key.proof.ProofTreeListener#proofExpanded(de.uka.ilkd.key.proof.ProofTreeEvent)
319: */
320: public void proofExpanded(ProofTreeEvent e) {
321: // nothing, this is not important for the list of goals
322: }
323:
324: /**
325: * invoked if all goals of the proof are closed
326: */
327: public void proofClosed(ProofTreeEvent e) {
328: setAttentive(true);
329: clear();
330: }
331:
332: /** The proof tree has been pruned under the node mentioned in the
333: * ProofTreeEvent. In other words, that node should no longer
334: * have any children now. Any nodes that were not descendants of
335: * that node are unaffected.*/
336: public void proofPruned(ProofTreeEvent e) {
337: clear();
338: add(e.getSource().openGoals());
339: }
340:
341: /** invoked if the list of goals changed (goals were added,
342: * removed etc.
343: */
344: public void proofGoalRemoved(ProofTreeEvent e) {
345: remove(e.getGoal());
346: }
347:
348: /** invoked if the current goal of the proof changed */
349: public void proofGoalsAdded(ProofTreeEvent e) {
350: add(e.getGoals());
351: }
352:
353: /** invoked if the current goal of the proof changed */
354: public void proofGoalsChanged(ProofTreeEvent e) {
355: clear();
356: add(e.getGoals());
357: }
358:
359: public void proofStructureChanged(ProofTreeEvent e) {
360: clear();
361: add(e.getSource().openGoals());
362: }
363: }
364: }
365:
366: /**
367: * Decorate <code>GoalListModel</code> with a filter that hides certain
368: * goals. This is currently used to prevent the display of goals that appear
369: * closed for the present user constraint.
370: */
371: private class SelectingGoalListModel extends AbstractListModel {
372:
373: private final GoalListModel delegate;
374: /**
375: * The last known size of the delegate model. This is used to recognise
376: * addition or removal of rows
377: */
378: private int delegateSize;
379:
380: private Proof proof = null;
381: /**
382: * Listen for modification of the user constraint
383: */
384: private final UCListener ucListener = new UCListener();
385:
386: /**
387: * List of <code>Integer</code> objects that determine the (strictly
388: * monotonic) mapping of the row indexes of this model to the rows of
389: * the delegate model
390: */
391: private final ArrayList entries = new ArrayList(10);
392: private final DelegateListener delegateListener = new DelegateListener();
393:
394: public SelectingGoalListModel(GoalListModel delegate) {
395: this .delegate = delegate;
396: }
397:
398: public int getSize() {
399: return entries.size();
400: }
401:
402: public Object getElementAt(int i) {
403: if (i < 0 || i >= getSize())
404: return null;
405: return delegate.getElementAt(getDelegateIndex(i));
406: }
407:
408: private int getDelegateIndex(int i) {
409: return ((Integer) entries.get(i)).intValue();
410: }
411:
412: /**
413: * the proof this view belongs to has changed; this also updates the
414: * delegate model
415: */
416: protected void setProof(Proof p) {
417: delegate.removeListDataListener(delegateListener);
418:
419: if (proof != null) {
420: proof.getUserConstraint()
421: .removeConstraintTableListener(ucListener);
422: }
423: proof = p;
424: if (proof != null) {
425: proof.getUserConstraint().addConstraintTableListener(
426: ucListener);
427: }
428:
429: delegate.setProof(p);
430: setup();
431:
432: delegate.addListDataListener(delegateListener);
433: }
434:
435: private boolean isHiddenGoal(final Goal goal) {
436: return proof != null
437: && proof.getUserConstraint().displayClosed(
438: goal.node());
439: }
440:
441: private void setup() {
442: entries.clear();
443: selectFromInterval(0, delegate.getSize());
444: updateDelegateSize();
445: fireContentsChanged(this , 0, getSize() - 1);
446: selectSelectedGoal(); // this should rather be done by modifying the SelectionModel
447: }
448:
449: /**
450: * Determine the visible goals of a certain interval [delegateBegin,
451: * delegateEnd) of the delegate model and create the respective entries
452: * of the selection mapping
453: *
454: * @return the first position of the mapping after the added parts
455: */
456: private int selectFromInterval(int delegateBegin,
457: int delegateEnd) {
458: // defensive
459: delegateEnd = Math.min(delegateEnd, delegate.getSize());
460:
461: int ind = delegatePosToMappingPos(delegateBegin);
462:
463: for (int i = delegateBegin; i < delegateEnd; ++i) {
464: final Goal goal = (Goal) delegate.getElementAt(i);
465: if (!isHiddenGoal(goal))
466: entries.add(ind++, new Integer(i));
467: }
468:
469: return ind;
470: }
471:
472: /**
473: * Remove the parts of the entry mapping for a certain interval
474: * [delegateBegin, delegateEnd) of the delegate model
475: *
476: * @return the first position of the mapping after the removed parts
477: */
478: private int removeInterval(int delegateBegin, int delegateEnd) {
479: final int ind = delegatePosToMappingPos(delegateBegin);
480:
481: int removeCount = 0;
482: while (ind != entries.size()
483: && getDelegateIndex(ind) < delegateEnd) {
484: entries.remove(ind);
485: ++removeCount;
486: }
487:
488: return ind;
489: }
490:
491: private int delegatePosToMappingPos(int delegateIndex) {
492: // unefficient, could be implemented using binary search (is there
493: // an usable algorithm for this purpose in the Java library?)
494:
495: for (int res = 0; res != entries.size(); ++res) {
496: if (getDelegateIndex(res) >= delegateIndex)
497: return res;
498: }
499: return entries.size();
500: }
501:
502: /**
503: * Shift values of the entries [begin, getSize()) of the selection
504: * mapping by the given amount
505: */
506: private void shiftTail(int begin, int amount) {
507: for (; begin != entries.size(); ++begin)
508: entries.set(begin, new Integer(getDelegateIndex(begin)
509: + amount));
510: }
511:
512: private int delegateSizeChange() {
513: return delegate.getSize() - delegateSize;
514: }
515:
516: private void updateDelegateSize() {
517: delegateSize = delegate.getSize();
518: }
519:
520: private class DelegateListener implements ListDataListener {
521: private int delegateBegin(ListDataEvent e) {
522: return e.getIndex0();
523: }
524:
525: private int delegateEnd(ListDataEvent e) {
526: return e.getIndex1() + 1; // we are calculating with right-open intervals
527: }
528:
529: public void contentsChanged(ListDataEvent e) {
530: // this method is currently not used by the delegate and thus
531: // not sufficiently tested
532:
533: final int oldDelegateEnd = delegateEnd(e)
534: - delegateSizeChange();
535: final int begin = removeInterval(delegateBegin(e),
536: oldDelegateEnd);
537:
538: shiftTail(begin, delegateSizeChange());
539:
540: final int end = selectFromInterval(delegateBegin(e),
541: delegateEnd(e));
542:
543: updateDelegateSize();
544:
545: final int changeBegin = begin;
546: final int changeEnd = end - 1;
547: if (changeEnd >= changeBegin)
548: fireContentsChanged(this , changeBegin, changeEnd);
549: selectSelectedGoal(); // this should rather be done by modifying the SelectionModel
550: }
551:
552: public void intervalAdded(ListDataEvent e) {
553: final int oldSize = entries.size();
554: final int end = selectFromInterval(delegateBegin(e),
555: delegateEnd(e));
556: shiftTail(end, delegateSizeChange());
557:
558: updateDelegateSize();
559:
560: final int addBegin = end - (entries.size() - oldSize);
561: final int addEnd = end - 1;
562: if (addEnd >= addBegin)
563: fireIntervalAdded(this , addBegin, addEnd);
564: selectSelectedGoal(); // this should rather be done by modifying
565: // the SelectionModel
566: }
567:
568: public void intervalRemoved(ListDataEvent e) {
569: final int oldSize = entries.size();
570: final int begin = removeInterval(delegateBegin(e),
571: delegateEnd(e));
572: shiftTail(begin, delegateSizeChange());
573:
574: updateDelegateSize();
575:
576: final int remBegin = begin;
577: final int remEnd = begin + (oldSize - entries.size())
578: - 1;
579: if (remEnd >= remBegin)
580: fireIntervalRemoved(this , remBegin, remEnd);
581: selectSelectedGoal(); // this should rather be done by modifying
582: // the SelectionModel
583: }
584: }
585:
586: private class UCListener implements ConstraintTableListener {
587:
588: /*
589: * (non-Javadoc)
590: *
591: * @see de.uka.ilkd.key.proof.ConstraintTableListener#constraintChanged(de.uka.ilkd.key.proof.ConstraintTableEvent)
592: */
593: public void constraintChanged(ConstraintTableEvent e) {
594: setup();
595: }
596: }
597: }
598:
599: private final static int MAX_DISPLAYED_SEQUENT_LENGTH = 100;
600:
601: // clear this cache whenever some display settings are changed?
602: private final WeakHashMap seqToString = new WeakHashMap();
603:
604: private String seqToString(Sequent seq) {
605: String res = (String) seqToString.get(seq);
606: if (res == null) {
607: LogicPrinter sp = new LogicPrinter(
608: new ProgramPrinter(null), mediator()
609: .getNotationInfo(), mediator()
610: .getServices(), true);
611: seq.prettyprint(sp);
612: res = sp.toString().replace('\n', ' ');
613: res = res.substring(0, Math.min(
614: MAX_DISPLAYED_SEQUENT_LENGTH, res.length()));
615:
616: seqToString.put(seq, res);
617: }
618: return res;
619: }
620:
621: private class IconCellRenderer extends DefaultListCellRenderer
622: implements ListCellRenderer, java.io.Serializable {
623:
624: public IconCellRenderer() {
625: GoalList.this .setToolTipText("GOAL");
626: }
627:
628: public Component getListCellRendererComponent(JList list,
629: Object value, // value to display
630: int index, // cell index
631: boolean isSelected, // is the cell selected
632: boolean cellHasFocus) // the list and the cell have the focus
633: {
634: String valueStr;
635: Color col = Color.black;
636: if (value instanceof Goal) {
637: final Sequent seq = ((Goal) value).sequent();
638: valueStr = seqToString(seq);
639:
640: if (((Goal) value).getClosureConstraint()
641: .isSatisfiable())
642: col = Color.blue;
643: } else {
644: valueStr = "" + value;
645: }
646: DefaultListCellRenderer sup = (DefaultListCellRenderer) super
647: .getListCellRendererComponent(list, valueStr,
648: index, isSelected, cellHasFocus);
649: sup.setIcon(keyIcon);
650:
651: // set color according to closure status
652: sup.setForeground(col);
653:
654: return sup;
655: }
656: }
657: }
|