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.nodeviews;
009:
010: import java.io.StringWriter;
011: import java.io.Writer;
012:
013: import javax.swing.JMenuItem;
014:
015: import de.uka.ilkd.key.gui.configuration.ProofSettings;
016: import de.uka.ilkd.key.pp.LogicPrinter;
017: import de.uka.ilkd.key.pp.NotationInfo;
018: import de.uka.ilkd.key.pp.ProgramPrinter;
019: import de.uka.ilkd.key.rule.TacletApp;
020: import de.uka.ilkd.key.util.pp.WriterBackend;
021:
022: /**
023: * this class extends JMenuItem. The objective is to store
024: * the Taclet of each item in the item for easier access to the Taclet
025: * if the item has been selected
026: */
027: class DefaultTacletMenuItem extends JMenuItem implements TacletMenuItem {
028:
029: private TacletApp connectedTo;
030:
031: /** creates TacletMenuItem attached to a Taclet
032: * @param connectedTo the TacletApp that is represented by the item
033: * @param notationInfo the NotationInfo used to print terms
034: */
035: public DefaultTacletMenuItem(JMenuItem menu, TacletApp connectedTo,
036: NotationInfo notationInfo) {
037: super (connectedTo.taclet().displayName());
038: this .connectedTo = connectedTo;
039: StringBuffer taclet_sb = new StringBuffer();
040: Writer w = new StringWriter();
041:
042: WriterBackend backend = new WriterBackend(w, 68);
043: LogicPrinter tp = new LogicPrinter(new ProgramPrinter(w,
044: connectedTo.instantiations()), notationInfo, backend,
045: null, true);
046: tp.printTaclet(connectedTo.taclet(), connectedTo
047: .instantiations(), ProofSettings.DEFAULT_SETTINGS
048: .getViewSettings().getShowWholeTaclet());
049:
050: int nlcount = 0;
051: StringBuffer sb = new StringBuffer(w.toString());
052: int sbl = sb.length();
053: for (int i = 0; i < sbl; i++) {
054: if (sb.charAt(i) == '\n') {
055: nlcount += 1;
056: }
057: }
058: if (nlcount > ProofSettings.DEFAULT_SETTINGS.getViewSettings()
059: .getMaxTooltipLines()) {
060: if (TacletMenu.logger.isDebugEnabled()) {
061: TacletMenu.logger
062: .debug("No SchemaVariable instantiation printed, linecount is "
063: + nlcount
064: + " > "
065: + ProofSettings.DEFAULT_SETTINGS
066: .getViewSettings()
067: .getMaxTooltipLines());
068: }
069: taclet_sb = new StringBuffer();
070: w = new StringWriter();
071: backend = new WriterBackend(w, 68);
072: tp = new LogicPrinter(new ProgramPrinter(w), notationInfo,
073: backend, null, true);
074: tp.printTaclet(connectedTo.taclet());
075:
076: }
077:
078: taclet_sb.append(ascii2html(new StringBuffer(w.toString())));
079: taclet_sb.replace(0, 0, "<html><pre>");
080: taclet_sb.append("</pre>");
081:
082: setToolTipText(taclet_sb.toString());
083: }
084:
085: /**
086: * Replaces <,>,& and new lines with their HTML masks.
087: * @param sb The StringBuffer with forbidden HTML characters
088: * @return A new StringBuffer with the masked characters.
089: */
090: protected StringBuffer ascii2html(StringBuffer sb) {
091: StringBuffer nsb = new StringBuffer();
092: StringBuffer asb = removeEmptyLines(sb);
093: int sbl = asb.length();
094: for (int i = 0; i < sbl; i++) {
095: switch (asb.charAt(i)) {
096: case '<':
097: nsb.append("<");
098: break;
099: case '>':
100: nsb.append(">");
101: break;
102: case '&':
103: nsb.append("&");
104: break;
105: case '\n':
106: nsb.append("<br>");
107: break;
108: default:
109: nsb.append(asb.charAt(i));
110: }
111: }
112: return nsb;
113: }
114:
115: protected StringBuffer removeEmptyLines(StringBuffer sb) {
116: String s = sb.toString();
117: String[] sa = s.split("\n");
118: StringBuffer result = new StringBuffer();
119: for (int i = 0; i < sa.length; i++) {
120: //logger.debug("'" + sa[i] + "'");
121: if (sa[i] == "") {
122: continue;
123: }
124: boolean onlySpaces = true;
125: for (int j = 0; j < sa[i].length(); j++) {
126: if (sa[i].charAt(j) != ' ') {
127: onlySpaces = false;
128: }
129: }
130: if (onlySpaces) {
131: continue;
132: }
133: result.append(sa[i]).append("\n");
134: }
135: if (result.charAt(result.length() - 1) == '\n') {
136: result.setLength(result.length() - 1);
137: }
138: return result;
139: }
140:
141: /* (non-Javadoc)
142: * @see de.uka.ilkd.key.gui.TacletMenuItem#connectedTo()
143: */
144: public TacletApp connectedTo() {
145: return connectedTo;
146: }
147:
148: }
|