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.nodeviews;
012:
013: import java.awt.*;
014: import java.awt.dnd.Autoscroll;
015: import java.awt.dnd.DnDConstants;
016: import java.awt.dnd.DragSource;
017: import java.awt.dnd.DropTarget;
018: import java.awt.event.ComponentEvent;
019: import java.awt.event.ComponentListener;
020: import java.awt.event.HierarchyBoundsListener;
021: import java.awt.event.HierarchyEvent;
022: import java.beans.PropertyChangeEvent;
023: import java.beans.PropertyChangeListener;
024: import java.util.HashMap;
025: import java.util.Iterator;
026: import java.util.Vector;
027:
028: import javax.swing.JEditorPane;
029: import javax.swing.SwingUtilities;
030: import javax.swing.UIManager;
031: import javax.swing.text.BadLocationException;
032: import javax.swing.text.DefaultHighlighter;
033: import javax.swing.text.Highlighter.HighlightPainter;
034:
035: import de.uka.ilkd.key.gui.ApplyTacletDialog;
036: import de.uka.ilkd.key.gui.GUIEvent;
037: import de.uka.ilkd.key.gui.GUIListener;
038: import de.uka.ilkd.key.gui.KeYMediator;
039: import de.uka.ilkd.key.gui.configuration.Config;
040: import de.uka.ilkd.key.gui.configuration.ConfigChangeEvent;
041: import de.uka.ilkd.key.gui.configuration.ConfigChangeListener;
042: import de.uka.ilkd.key.logic.Sequent;
043: import de.uka.ilkd.key.pp.LogicPrinter;
044: import de.uka.ilkd.key.pp.PosInSequent;
045: import de.uka.ilkd.key.pp.Range;
046: import de.uka.ilkd.key.pp.SequentPrintFilter;
047: import de.uka.ilkd.key.rule.TacletApp;
048: import de.uka.ilkd.key.util.Debug;
049:
050: /**
051: * The sequent view displays the sequent of an open goal and allows selection of
052: * formulas as well as the application of rules. It offers services for highlighting
053: * formulas, selecting applicable rules (in particular taclets) and drag'n drop
054: * instantiation of taclets.
055: */
056: public class SequentView extends JEditorPane implements Autoscroll {
057:
058: public static final Color DEFAULT_HIGHLIGHT_COLOR = Color.yellow;
059:
060: public static final Color UPDATE_HIGHLIGHT_COLOR = new Color(255,
061: 230, 230);
062:
063: // the default tag of the highlight
064: private Object defaultHighlight;
065:
066: // the current tag of the highlight
067: private Object currentHighlight;
068:
069: // an additional highlight to mark the first active statement
070: private Object additionalHighlight;
071:
072: // a vector of highlights to mark updates
073: private Vector updateHighlights;
074:
075: // all known highlights
076: private HashMap color2Highlight = new HashMap();
077:
078: // the used sequentprinter
079: private LogicPrinter printer;
080:
081: // the used sequent filter
082: private SequentPrintFilter filter;
083:
084: // the current line width
085: int lineWidth;
086:
087: // the used sequent
088: private Sequent seq;
089:
090: // the mediator
091: private KeYMediator mediator;
092:
093: // the mouse/mouseMotion listener
094: protected SequentViewListener listener;
095:
096: // a component and property change listener used to
097: // update the sequent view on font or size changes
098: private SeqViewChangeListener changeListener;
099:
100: // an object that detects opening and closing of an Taclet instantiation dialog
101: private GUIListener guiListener;
102:
103: // enables this component to be a Drag Source
104: DragSource dragSource = null;
105:
106: // last highlighted caret position
107: private int lastHighlightedCaretPos;
108:
109: private static final Insets autoScrollSensitiveRegion = new Insets(
110: 20, 20, 20, 20);
111:
112: /**
113: * creates a viewer for a sequent
114: * @param mediator the KeYMediator allowing access to the
115: * current system status
116: */
117: public SequentView(KeYMediator mediator) {
118: /* setting this to text/html causes the position tables to go wrong */
119: super ("text/plain", "");
120: setMediator(mediator);
121: // view cannot be edited
122: setEditable(false);
123: // disables selection
124: setSelectionColor(getBackground());
125: // sets the painter for the highlightning
126: setHighlighter(new DefaultHighlighter());
127: //sets initial highlight (not visible) and stores its tag
128:
129: // REMARK: THE ORDER FOR ADDING HIGHLIGHTS IS CRUCIAL
130: // WHEN USING OVERLAPPING HIGHLIGHTS:
131: // Adding highlight H1 before highlight H2 ensures that
132: // H1 can overwrite overlapping parts of H2 !!!
133:
134: additionalHighlight = getColorHighlight(Color.lightGray);
135: defaultHighlight = getColorHighlight(DEFAULT_HIGHLIGHT_COLOR);
136:
137: currentHighlight = defaultHighlight;
138: updateHighlights = new Vector();
139:
140: Config.DEFAULT
141: .addConfigChangeListener(new ConfigChangeListener() {
142: public void configChanged(ConfigChangeEvent e) {
143: updateUI();
144: }
145: });
146:
147: setSequentViewFont();
148:
149: listener = new SequentViewListener(this , mediator());
150:
151: guiListener = new GUIListener() {
152: /** invoked if a frame that wants modal access is opened */
153: public void modalDialogOpened(GUIEvent e) {
154:
155: if (e.getSource() instanceof ApplyTacletDialog) {
156: // enable drag'n'drop ...
157: listener.setModalDragNDropEnabled(true);
158: listener.setRefreshHighlightning(true);
159:
160: } else {
161: // disable drag'n'drop and highlightning ...
162: listener.setModalDragNDropEnabled(false);
163: listener.setRefreshHighlightning(false);
164: }
165:
166: // disable drag and drop instantiation of taclets
167: getDropTarget().setActive(false);
168: }
169:
170: /** invoked if a frame that wants modal access is closed */
171: public void modalDialogClosed(GUIEvent e) {
172: if (e.getSource() instanceof ApplyTacletDialog) {
173: // disable drag'n'drop ...
174: listener.setModalDragNDropEnabled(false);
175: listener.setRefreshHighlightning(true);
176: } else {
177: listener.setRefreshHighlightning(true);
178: }
179:
180: // enable drag and drop instantiation of taclets
181: getDropTarget().setActive(true);
182: }
183:
184: /** invoked if the user wants to abort the proving session */
185: public void shutDown(GUIEvent e) {
186: }
187: };
188:
189: addMouseListener(listener);
190: addMouseMotionListener(listener);
191: addKeyListener(listener);
192:
193: // and here comes the drag'n'drop stuff that allows the user to copy
194: // the currently highlighted subterm/formula by mere drag'n'dop actions
195:
196: dragSource = new DragSource();
197:
198: dragSource.createDefaultDragGestureRecognizer(this ,
199: DnDConstants.ACTION_COPY, listener
200: .getDragGestureListener());
201:
202: // And now the Drag'n'drop stuff ...
203:
204: final DragNDropInstantiator dragNDropInstantiator = new DragNDropInstantiator(
205: this );
206: final DropTarget aDropTarget = new DropTarget(this ,
207: dragNDropInstantiator);
208:
209: this .setAutoscrolls(true);
210: this .setDropTarget(aDropTarget);
211:
212: // add listener to KeY GUI events
213: mediator().addGUIListener(guiListener);
214:
215: // add a listener to this component
216: changeListener = new SeqViewChangeListener();
217: addComponentListener(changeListener);
218: addPropertyChangeListener("font", changeListener);
219:
220: addHierarchyBoundsListener(changeListener);
221:
222: }
223:
224: protected DragSource getDragSource() {
225: return dragSource;
226: }
227:
228: /**
229: * returns the default tag used for highligthing
230: * @return the default tag used for highlighting
231: */
232: public Object getDefaultHighlight() {
233: return defaultHighlight;
234: }
235:
236: /**
237: * sets the correct highlighter for the given color
238: * @param tag the Object used as tag for highlighting
239: */
240: public void setCurrentHighlight(Object tag) {
241: currentHighlight = tag;
242: }
243:
244: /**
245: * returns the current tag used for highligthing
246: * @return the current tag used for highlighting
247: */
248: public Object getCurrentHighlight() {
249: return currentHighlight;
250: }
251:
252: /**
253: * updates all updateHighlights. Firstly removes all displayed ones and
254: * then gets a new list of updates to highlight
255: */
256: public void updateUpdateHighlights() {
257: if (printer == null)
258: return;
259:
260: Iterator it = updateHighlights.iterator();
261:
262: while (it.hasNext()) {
263: removeHighlight(it.next());
264: }
265:
266: updateHighlights.clear();
267: Range[] ranges = printer.getPositionTable().getUpdateRanges();
268:
269: if (ranges != null) {
270: for (int i = 0; i < ranges.length; i++) {
271: Object tag = getColorHighlight(UPDATE_HIGHLIGHT_COLOR);
272: updateHighlights.addElement(tag);
273: paintHighlight(ranges[i], tag);
274: }
275: }
276: }
277:
278: /**
279: * removes highlight by setting it to position (0,0)
280: */
281: public void disableHighlight(Object highlight) {
282: try {
283: getHighlighter().changeHighlight(highlight, 0, 0);
284: } catch (BadLocationException e) {
285: Debug.out("Invalid range for highlight");
286: }
287: }
288:
289: /**
290: * removes the term and first statement highlighter by setting them to
291: * position (0,0)
292: */
293: public void disableHighlights() {
294: disableHighlight(currentHighlight);
295: disableHighlight(additionalHighlight);
296: }
297:
298: /**
299: * returns the highlight painter for the specified color
300: * @param color the Color the HighlightPainter shall use
301: * @return the highlight painter for the specified color
302: */
303: private HighlightPainter getColorHighlightPainter(Color color) {
304: if (!color2Highlight.containsKey(color)) {
305: color2Highlight.put(color,
306: new DefaultHighlighter.DefaultHighlightPainter(
307: color));
308: }
309: return (HighlightPainter) color2Highlight.get(color);
310: }
311:
312: /**
313: * registers a highlighter that marks the regions specified by the returned
314: * tag with the given color
315: * @param color the Color used to highlight regions of the sequent
316: * @return the highlight for the specified color
317: */
318: public Object getColorHighlight(Color color) {
319: Object highlight = null;
320: try {
321: highlight = getHighlighter().addHighlight(0, 0,
322: getColorHighlightPainter(color));
323: } catch (BadLocationException e) {
324: Debug.out("Highlight range out of scope.");
325: }
326: return highlight;
327: }
328:
329: /**
330: * d a highlighter that marks the regions specified by the returned
331: * tag with the given color
332: * @param highlight the Object used as tag for the highlight
333: */
334: public void removeHighlight(Object highlight) {
335: getHighlighter().removeHighlight(highlight);
336: }
337:
338: public void updateUI() {
339: super .updateUI();
340: setSequentViewFont();
341: }
342:
343: private void setSequentViewFont() {
344: Font myFont = UIManager
345: .getFont(Config.KEY_FONT_CURRENT_GOAL_VIEW);
346: if (myFont != null) {
347: setFont(myFont);
348: } else {
349: Debug
350: .out("KEY_FONT_CURRENT_GOAL_VIEW not available. Use standard font.");
351: }
352: }
353:
354: /** sets the text being printed */
355: public synchronized void printSequent() {
356: if (SwingUtilities.isEventDispatchThread()) {
357: printSequentImmediately();
358: } else {
359: Runnable sequentUpdater = new Runnable() {
360: public void run() {
361: printSequentImmediately();
362: }
363: };
364: SwingUtilities.invokeLater(sequentUpdater);
365: }
366: }
367:
368: /**
369: * computes the line width
370: */
371: private int computeLineWidth() {
372: // assumes we have a uniform font width
373: int maxChars = (int) (getVisibleRect().getWidth() / getFontMetrics(
374: getFont()).charWidth('W'));
375:
376: if (maxChars > 1)
377: maxChars -= 1;
378:
379: return maxChars;
380: }
381:
382: /** sets the text being printed */
383: public synchronized void printSequentImmediately() {
384: removeMouseMotionListener(listener);
385: removeMouseListener(listener);
386:
387: lineWidth = computeLineWidth();
388:
389: if (printer != null) {
390: printer.update(seq, filter, lineWidth);
391: boolean errorocc;
392: do {
393: errorocc = false;
394: try {
395: setText(printer.toString());
396: } catch (Error e) {
397: System.err
398: .println("Error occurred while printing Sequent!");
399: errorocc = true;
400: }
401: } while (errorocc);
402: }
403:
404: restorePosition();
405: updateUpdateHighlights();
406:
407: addMouseMotionListener(listener);
408: addMouseListener(listener);
409:
410: repaint();
411: }
412:
413: /** makes the last caret position visible (if possible) */
414: private void restorePosition() {
415: int lastCaretPos = getLastHighlightedCaretPos();
416: if (!(lastCaretPos < 0 || getDocument() == null || lastCaretPos > getDocument()
417: .getLength())) {
418: setCaretPosition(lastCaretPos);
419: }
420: }
421:
422: void setLastHighlightedCaretPos(int pos) {
423: lastHighlightedCaretPos = pos;
424: }
425:
426: int getLastHighlightedCaretPos() {
427: return lastHighlightedCaretPos;
428: }
429:
430: /** sets the LogicPrinter to use
431: * @param sp the LogicPrinter that is used
432: */
433: public void setPrinter(LogicPrinter sp, Sequent s) {
434: setPrinter(sp, null, s);
435: }
436:
437: // xxx remove?
438: protected SequentPrintFilter getSequentPrintFilter() {
439: return filter;
440: }
441:
442: /** sets the LogicPrinter to use
443: * @param sp the LogicPrinter that is used
444: * @param f the SequentPrintFilter that is used
445: */
446: public void setPrinter(LogicPrinter sp, SequentPrintFilter f,
447: Sequent s) {
448: printer = sp;
449: filter = f;
450: seq = s;
451: }
452:
453: /** return used LogicPrinter
454: * @return the LogicPrinter that is used
455: */
456: public LogicPrinter printer() {
457: return printer;
458: }
459:
460: /** sets the mediator
461: * @param mediator the KeYMediator used to communicate with other
462: * components
463: */
464: private void setMediator(KeYMediator mediator) {
465: Debug.assertTrue(mediator != null, "Mediator must be set");
466: this .mediator = mediator;
467: }
468:
469: /** the startposition and endposition+1 of the string to be
470: * highlighted
471: * @param p the mouse pointer coordinates
472: */
473: public void paintHighlights(Point p) {
474: // Change highlight for additional Java statement ...
475: paintHighlight(getFirstStatementRange(p), additionalHighlight);
476: // Change Highlighter for currently selected sequent part
477: paintHighlight(getHighlightRange(p), currentHighlight);
478: }
479:
480: /**
481: * highlights the elements in the given range using the specified
482: * highlighter
483: * @param range the Range to be highlighted
484: * @param highlighter the Object painting the highlight
485: */
486: void paintHighlight(Range range, Object highlighter) {
487: try {
488: // Change highlight for additional Java statement ...
489: if (range != null) {
490: getHighlighter().changeHighlight(highlighter,
491: range.start(), range.end());
492: } else {
493: getHighlighter().changeHighlight(highlighter, 0, 0);
494: }
495: } catch (BadLocationException badLocation) {
496: System.err.println("SequentView tried to highlight an area"
497: + "that is not existing.");
498: System.err.println("Exception:" + badLocation);
499: }
500: }
501:
502: /** returns the mediator of this view
503: * @return the KeYMediator
504: */
505: public KeYMediator mediator() {
506: return mediator;
507: }
508:
509: /** selected rule to apply
510: * @param taclet the selected Taclet
511: * @param pos the PosInSequent describes the position where to apply the
512: * rule
513: */
514: void selectedTaclet(TacletApp taclet, PosInSequent pos) {
515: mediator().selectedTaclet(taclet, pos);
516: }
517:
518: /**
519: * Enables drag'n'drop of highlighted subterms in the sequent window.
520: * @param allowDragNDrop enables drag'n'drop iff set to true.
521: */
522: public synchronized void setModalDragNDropEnabled(
523: boolean allowDragNDrop) {
524: listener.setModalDragNDropEnabled(allowDragNDrop);
525: }
526:
527: /**
528: * Checks whether drag'n'drop of highlighted subterms in the sequent window
529: * currently is enabled..
530: * @return true iff drag'n'drop is enabled.
531: */
532: public synchronized boolean modalDragNDropEnabled() {
533: return listener.modalDragNDropEnabled();
534: }
535:
536: public String getHighlightedText() {
537: String s;
538: try {
539: PosInSequent pos = listener.getMousePos();
540: s = getText(pos.getBounds().start(), pos.getBounds()
541: .length());
542: } catch (Exception ble) { // whatever it is -- forget about it
543: s = "";
544: }
545: return s;
546: }
547:
548: public PosInSequent getMousePosInSequent() {
549: return listener.getMousePos();
550: }
551:
552: /** Get a PosInSequent object for a given coordinate of the
553: * displayed sequent. */
554: protected synchronized PosInSequent getPosInSequent(Point p) {
555: String seqText = getText();
556: if (seqText.length() > 0) {
557: int characterIndex = correctedViewToModel(p);
558:
559: return printer().getPositionTable().getPosInSequent(
560: characterIndex, filter);
561: } else {
562: return null;
563: }
564: }
565:
566: /** Get the character range to be highlighted for the given
567: * coordinate in the displayed sequent. */
568: synchronized Range getHighlightRange(Point p) {
569: String seqText = getText();
570: if (seqText.length() > 0) {
571: int characterIndex = correctedViewToModel(p);
572: return printer().getPositionTable().rangeForIndex(
573: characterIndex);
574: } else {
575: return null;
576: }
577: }
578:
579: /** Get the character range to be highlighted for the first
580: * statement in a java block at the given
581: * coordinate in the displayed sequent. Returns null
582: * if there is no java block there.*/
583: protected synchronized Range getFirstStatementRange(Point p) {
584: String seqText = getText();
585: if (seqText.length() > 0) {
586: int characterIndex = correctedViewToModel(p);
587:
588: return printer().getPositionTable()
589: .firstStatementRangeForIndex(characterIndex);
590: } else {
591: return null;
592: }
593: }
594:
595: /** Return the character index for a certain coordinate. The
596: * usual viewToModel is focussed on inter-character spaces, not
597: * characters, so it returns the correct index in the
598: * left half of the glyph but one too many in the right half.
599: * Therefore, we get width of character before the one given
600: * by viewToModel, substract it from the given x value, and get
601: * the character at the new position. That is the correct one.
602: */
603: public int correctedViewToModel(Point p) {
604: String seqText = getText();
605:
606: int cursorPosition = viewToModel(p);
607:
608: cursorPosition -= (cursorPosition > 0 ? 1 : 0);
609:
610: cursorPosition = (cursorPosition >= seqText.length() ? seqText
611: .length() - 1 : cursorPosition);
612: cursorPosition = (cursorPosition >= 0 ? cursorPosition : 0);
613: int previousCharacterWidth = getFontMetrics(getFont())
614: .charWidth(seqText.charAt(cursorPosition));
615:
616: int characterIndex = viewToModel(new Point((int) p.getX()
617: - (previousCharacterWidth / 2), (int) p.getY()));
618:
619: return characterIndex;
620: }
621:
622: /**
623: * used for autoscrolling when performing drag and drop actions.
624: * Computes the rectangle to be made visible.
625: */
626: public void autoscroll(Point loc) {
627: final Insets insets = getAutoscrollInsets();
628: final Rectangle outer = getVisibleRect();
629: final Rectangle inner = new Rectangle(outer.x + insets.left,
630: outer.y + insets.top, outer.width
631: - (insets.left + insets.right), outer.height
632: - (insets.top + insets.bottom));
633:
634: if (!inner.contains(loc)) {
635: Rectangle scrollRect = new Rectangle(loc.x - insets.left,
636: loc.y - insets.top, insets.left + insets.right,
637: insets.top + insets.bottom);
638: scrollRectToVisible(scrollRect);
639: }
640: }
641:
642: /**
643: * used to define the area in which autoscrolling will be
644: * initialized
645: */
646: public Insets getAutoscrollInsets() {
647: return autoScrollSensitiveRegion;
648: }
649:
650: private class SeqViewChangeListener implements ComponentListener,
651: PropertyChangeListener, HierarchyBoundsListener {
652:
653: public void componentHidden(ComponentEvent e) {
654: }
655:
656: public void componentMoved(ComponentEvent e) {
657: }
658:
659: public void componentResized(ComponentEvent e) {
660: // reprint sequent
661: int lw = computeLineWidth();
662: if (lw != lineWidth) {
663: printSequent();
664: }
665: }
666:
667: public void componentShown(ComponentEvent e) {
668: }
669:
670: public void propertyChange(PropertyChangeEvent evt) {
671: // reprint sequent
672: printSequent();
673: }
674:
675: public void ancestorMoved(HierarchyEvent e) {
676: }
677:
678: public void ancestorResized(HierarchyEvent e) {
679: // reprint sequent
680: int lw = computeLineWidth();
681: if (lw != lineWidth) {
682: printSequent();
683: }
684: }
685: }
686:
687: }
|