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.Color;
014: import java.awt.Font;
015: import java.awt.Rectangle;
016:
017: import javax.swing.JTextArea;
018: import javax.swing.SwingUtilities;
019: import javax.swing.UIManager;
020: import javax.swing.plaf.TextUI;
021: import javax.swing.text.BadLocationException;
022: import javax.swing.text.DefaultHighlighter;
023: import javax.swing.text.Highlighter;
024: import javax.swing.text.Highlighter.HighlightPainter;
025:
026: import de.uka.ilkd.key.gui.KeYMediator;
027: import de.uka.ilkd.key.gui.configuration.Config;
028: import de.uka.ilkd.key.gui.configuration.ConfigChangeEvent;
029: import de.uka.ilkd.key.gui.configuration.ConfigChangeListener;
030: import de.uka.ilkd.key.logic.ListOfInteger;
031: import de.uka.ilkd.key.logic.PosInOccurrence;
032: import de.uka.ilkd.key.logic.PosInTerm;
033: import de.uka.ilkd.key.pp.*;
034: import de.uka.ilkd.key.proof.Node;
035: import de.uka.ilkd.key.rule.*;
036: import de.uka.ilkd.key.rule.inst.GenericSortInstantiations;
037: import de.uka.ilkd.key.util.Debug;
038: import de.uka.ilkd.key.rule.export.html.HTMLFileTaclet;
039:
040: public class NonGoalInfoView extends JTextArea {
041:
042: private LogicPrinter printer;
043: private SequentPrintFilter filter;
044:
045: public NonGoalInfoView(Node node, KeYMediator mediator) {
046: filter = new ConstraintSequentPrintFilter(node.sequent(),
047: mediator.getUserConstraint().getConstraint());
048: printer = new LogicPrinter(new ProgramPrinter(null), mediator
049: .getNotationInfo(), mediator.getServices());
050: printer.printSequent(null, filter);
051: String s = printer.toString();
052: RuleApp app = node.getAppliedRuleApp();
053: s += "\nNode Nr " + node.serialNr() + "\n";
054:
055: if (app != null) {
056: s = s + "\n \nUpcoming rule application: \n";
057: if (app.rule() instanceof Taclet) {
058: LogicPrinter tacPrinter = new LogicPrinter(
059: new ProgramPrinter(null), mediator
060: .getNotationInfo(), mediator
061: .getServices(), true);
062: tacPrinter.printTaclet((Taclet) (app.rule()));
063: s += tacPrinter;
064: } else {
065: s = s + app.rule();
066: }
067:
068: if (app instanceof TacletApp) {
069: TacletApp tapp = (TacletApp) app;
070: if (tapp.instantiations()
071: .getGenericSortInstantiations() != GenericSortInstantiations.EMPTY_INSTANTIATIONS) {
072: s = s + "\n\nWith sorts:\n";
073: s = s
074: + tapp.instantiations()
075: .getGenericSortInstantiations();
076: }
077:
078: StringBuffer sb = new StringBuffer("\n\n");
079: HTMLFileTaclet.writeTacletSchemaVariablesHelper(sb,
080: tapp.taclet());
081: s = s + sb;
082: }
083:
084: s = s + "\n\nApplication justified by: ";
085: s = s
086: + mediator.getSelectedProof().env().getJustifInfo()
087: .getJustification(app,
088: mediator.getServices()) + "\n";
089:
090: }
091:
092: /* Removed for the book version
093: s = s + "\nActive statement from:\n"+
094: node.getNodeInfo().getExecStatementParentClass()+":"+
095: node.getNodeInfo().getExecStatementPosition()+"\n";
096: */
097:
098: if (node.getReuseSource() != null) {
099: s += "\n" + node.getReuseSource().scoringInfo();
100: }
101:
102: Config.DEFAULT
103: .addConfigChangeListener(new ConfigChangeListener() {
104: public void configChanged(ConfigChangeEvent e) {
105: updateUI();
106: }
107: });
108:
109: updateUI();
110: setText(s);
111:
112: if (app != null) {
113: highlightRuleAppPosition(app);
114: } else {
115: // no rule app
116: setCaretPosition(0);
117: }
118:
119: setEditable(false);
120: }
121:
122: static final Highlighter.HighlightPainter RULEAPP_HIGHLIGHTER = new DefaultHighlighter.DefaultHighlightPainter(
123: new Color(0.5f, 1.0f, 0.5f));
124:
125: static final Highlighter.HighlightPainter IF_FORMULA_HIGHLIGHTER = new DefaultHighlighter.DefaultHighlightPainter(
126: new Color(0.8f, 1.0f, 0.8f));
127:
128: private void highlightRuleAppPosition(RuleApp app) {
129: try {
130: setHighlighter(new DefaultHighlighter());
131:
132: // Set the find highlight first and then the if highlights
133: // This seems to make cause the find one to be painted
134: // over the if one.
135:
136: final Range r;
137: if (app.posInOccurrence() == null) {
138: // rule does not have a find-part
139: r = null;
140: } else {
141: r = highlightPos(app.posInOccurrence(),
142: RULEAPP_HIGHLIGHTER);
143: }
144:
145: if (app instanceof TacletApp) {
146: highlightIfFormulas((TacletApp) app);
147: }
148:
149: if (r != null)
150: makeRangeVisible(r);
151: } catch (BadLocationException badLocation) {
152: System.err.println("NonGoalInfoView tried to "
153: + "highlight an area " + "that does not exist.");
154: System.err.println("Exception:" + badLocation);
155: }
156: }
157:
158: /**
159: * Ensure that the given range is visible
160: */
161: private void makeRangeVisible(final Range r) {
162: setCaretPosition(r.start());
163: final Runnable safeScroller = new Runnable() {
164: public void run() {
165: try {
166: final TextUI ui = getUI();
167: final NonGoalInfoView t = NonGoalInfoView.this ;
168: final Rectangle rect = ui.modelToView(t, r.start());
169: rect.add(ui.modelToView(t, r.end()));
170:
171: for (int i = 4; i >= 0; --i) {
172: final Rectangle rect2 = new Rectangle(rect);
173: final int border = i * 30;
174: rect2.add(rect.getMinX() - border, rect
175: .getMinY()
176: - border);
177: rect2.add(rect.getMaxX() + border, rect
178: .getMaxY()
179: + border);
180: scrollRectToVisible(rect2);
181: }
182: } catch (BadLocationException badLocation) {
183: System.err.println("NonGoalInfoView tried to "
184: + "make an area visible "
185: + "that does not exist.");
186: System.err.println("Exception:" + badLocation);
187: }
188: }
189: };
190: SwingUtilities.invokeLater(safeScroller);
191: }
192:
193: /**
194: * @param tapp The taclet app for which the if formulae
195: * should be highlighted.
196: * @throws BadLocationException
197: */
198: private void highlightIfFormulas(TacletApp tapp)
199: throws BadLocationException {
200: final ListOfIfFormulaInstantiation ifs = tapp
201: .ifFormulaInstantiations();
202: if (ifs == null)
203: return;
204: final IteratorOfIfFormulaInstantiation it = ifs.iterator();
205: while (it.hasNext()) {
206: final IfFormulaInstantiation inst2 = it.next();
207: if (!(inst2 instanceof IfFormulaInstSeq))
208: continue;
209: final IfFormulaInstSeq inst = (IfFormulaInstSeq) inst2;
210: final PosInOccurrence pos = new PosInOccurrence(inst
211: .getConstrainedFormula(), PosInTerm.TOP_LEVEL, inst
212: .inAntec());
213: final Range r = highlightPos(pos, IF_FORMULA_HIGHLIGHTER);
214: makeRangeVisible(r);
215: }
216: }
217:
218: /**
219: * @param pos the PosInOccurrence that should be highlighted.
220: * @param light the painter for the highlight.
221: * @return the range of characters that was highlighted.
222: * @throws BadLocationException
223: */
224: private Range highlightPos(PosInOccurrence pos,
225: HighlightPainter light) throws BadLocationException {
226: InitialPositionTable posTable = printer.getPositionTable();
227: ListOfInteger path = posTable.pathForPosition(pos, filter);
228: Range r = posTable.rangeForPath(path);
229: getHighlighter().addHighlight(r.start(), r.end(), light);
230: return r;
231: }
232:
233: public void updateUI() {
234: super .updateUI();
235: Font myFont = UIManager
236: .getFont(Config.KEY_FONT_INNER_NODE_VIEW);
237: if (myFont != null) {
238: setFont(myFont);
239: } else {
240: Debug
241: .out("KEY-INNER_NODE_FONT not available, use standard font.");
242: }
243: }
244: }
|