001: //Copyright (c) Hans-Joachim Daniels 2005
002: //
003: //This program is free software; you can redistribute it and/or modify
004: //it under the terms of the GNU General Public License as published by
005: //the Free Software Foundation; either version 2 of the License, or
006: //(at your option) any later version.
007: //
008: //This program is distributed in the hope that it will be useful,
009: //but WITHOUT ANY WARRANTY; without even the implied warranty of
010: //MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
011: //GNU General Public License for more details.
012: //
013: //You can either finde the file LICENSE or LICENSE.TXT in the source
014: //distribution or in the .jar file of this application
015:
016: package de.uka.ilkd.key.ocl.gf;
017:
018: import java.awt.Font;
019: import java.awt.Rectangle;
020: import java.util.Vector;
021:
022: import javax.swing.JEditorPane;
023:
024: /**
025: * @author daniels
026: * Takes care of collecting the linearized text and the length calculations
027: */
028: class Display {
029: /**
030: * If the linearization should be displayed as pure text
031: */
032: private boolean doText;
033: /**
034: * If the linearization should be displayed as HTML
035: */
036: private boolean doHtml;
037: /**
038: * collects the linearization after each append.
039: * what's in here are Strings
040: */
041: private Vector linStagesHtml = new Vector();
042: /**
043: * collects the linearization after each append.
044: * what's in here are Strings
045: */
046: private Vector linStagesText = new Vector();
047: /**
048: * Is used to calculate the length of a HTML snipplet.
049: * This pane is not displayed in hope to avoid any actual renderings
050: * which would just slow the length calculation down.
051: * Perhaps that's an abuse ...
052: * And perhaps this pane is not needed
053: */
054: private JEditorPane htmlLengthPane = new JEditorPane();
055:
056: /**
057: * initializes this object, nothing special
058: * @param dt 1 if only text is to be shown, 2 for only HTML, 3 for both.
059: * Other values are forbidden.
060: */
061: public Display(int dt) {
062: setDisplayType(dt);
063: this .htmlLengthPane.setContentType("text/html");
064: this .htmlLengthPane.setEditable(false);
065: }
066:
067: /**
068: * (de-)activates display of text and HTML according to dt
069: * @param dt 1 if only text is to be shown, 2 for only HTML, 3 for both.
070: */
071: protected void setDisplayType(int dt) {
072: switch (dt) {
073: case 1:
074: doText = true;
075: doHtml = false;
076: break;
077: case 2:
078: doText = false;
079: doHtml = true;
080: break;
081: case 3:
082: doText = true;
083: doHtml = true;
084: break;
085: default:
086: doText = true;
087: doHtml = true;
088: break;
089: }
090: }
091:
092: /**
093: * Resets the stored text, but leaves the scroll markers untouched.
094: */
095: public void resetLin() {
096: linStagesHtml.clear();
097: linStagesText.clear();
098: htmlLengthPane.setText("");
099: }
100:
101: /**
102: * @param font The Font, that is to be used. If null, the default of JTextPane is taken.
103: * @return the collected HTML text, that has been added to this object.
104: * <html> tags are wrapped around the result, if not already there.
105: */
106: protected String getHtml(Font font) {
107: if (!doHtml) {
108: return "";
109: }
110: String result;
111: if (this .linStagesHtml.size() > 0) {
112: String fontface;
113: if (font != null) {
114: //fontface = " style=\"font-size:" + font.getSize()+ "pt\"";
115: fontface = " style=\"font: " + font.getSize() + "pt "
116: + font.getName() + "\"";
117: } else {
118: fontface = "";
119: }
120: result = "<html><body"
121: + fontface
122: + ">"
123: + this .linStagesHtml.get(
124: this .linStagesHtml.size() - 1).toString()
125: + "</body></html>";
126: } else {
127: result = "";
128: }
129: return result;
130: }
131:
132: /**
133: * @return The collected pure text, that has been added to this object.
134: */
135: protected String getText() {
136: if (!doText) {
137: return "";
138: }
139: String result;
140: if (this .linStagesText.size() > 0) {
141: result = this .linStagesText.lastElement().toString();
142: } else {
143: result = "";
144: }
145: return result;
146: }
147:
148: /**
149: * Appends the given text to the respective fields from
150: * where it can be displayed later
151: * @param text The pure text that is to be appended.
152: * @param html The HTML text that is to be appended.
153: * Most likely the same as text
154: */
155: protected void addToStages(final String text, final String html) {
156: //add to HTML
157: if (doHtml) {
158: final String newStageHtml;
159: if (this .linStagesHtml.size() > 0) {
160: newStageHtml = this .linStagesHtml
161: .get(this .linStagesHtml.size() - 1)
162: + html;
163: } else {
164: newStageHtml = html;
165: }
166: this .linStagesHtml.add(newStageHtml);
167: }
168:
169: //add to Text
170: if (doText) {
171: final String newStageText;
172: if (this .linStagesText.size() > 0) {
173: newStageText = linStagesText
174: .get(linStagesText.size() - 1)
175: + text;
176: } else {
177: newStageText = text;
178: }
179: this .linStagesText.add(newStageText);
180: }
181: }
182:
183: /**
184: * Adds toAdd to both the pure text as the HTML fields, they are inherently the same,
185: * since they are mapped to the same position in the AST.
186: * On the way of adding, some length calculations are done, which are used to
187: * create an HtmlMarkedArea object, which is ready to be used in GFEditor2.
188: * @param toAdd The String that the to-be-produced MarkedArea should represent
189: * @param position The position String in Haskell notation
190: * @param language the language of the current linearization
191: * @return the HtmlMarkedArea object that represents the given information
192: * and knows about its beginning and end in the display areas.
193: */
194: protected MarkedArea addAsMarked(String toAdd,
195: LinPosition position, String language) {
196: /** the length of the displayed HTML before the current append */
197: int oldLengthHtml = 0;
198: if (doHtml) {
199: if (this .linStagesHtml.size() > 0) {
200: // is still in there. Does not absolutely need to be
201: // cached in a global variable
202: oldLengthHtml = this .htmlLengthPane.getDocument()
203: .getLength();
204: } else {
205: oldLengthHtml = 0;
206: }
207: }
208: /** the length of the text before the current append */
209: int oldLengthText = 0;
210: if (doText) {
211: if (this .linStagesText.size() > 0) {
212: // is still in there. Does not absolutely need to be
213: // cached in a global variable
214: oldLengthText = this .linStagesText.lastElement()
215: .toString().length();
216: } else {
217: oldLengthText = 0;
218: }
219: }
220: addToStages(toAdd, toAdd);
221: //calculate beginning and end
222: //for HTML
223: int newLengthHtml = 0;
224: if (doHtml) {
225: final String newStageHtml = this .linStagesHtml
226: .lastElement().toString();
227: final String newHtml = Printname.htmlPrepend(newStageHtml,
228: "");
229: //yeah, daniels admits, this IS expensive
230: this .htmlLengthPane.setText(newHtml);
231: newLengthHtml = htmlLengthPane.getDocument().getLength();
232: if (newLengthHtml < oldLengthHtml) {
233: newLengthHtml = oldLengthHtml;
234: }
235: }
236: //for text
237: int newLengthText = 0;
238: if (doText) {
239: newLengthText = this .linStagesText.lastElement().toString()
240: .length();
241: }
242: final MarkedArea hma = new MarkedArea(oldLengthText,
243: newLengthText, position, toAdd, oldLengthHtml,
244: newLengthHtml, language);
245: return hma;
246: }
247:
248: /**
249: * To store the scroll state of the pure text linearization area
250: */
251: Rectangle recText = new Rectangle();
252: /**
253: * To store the scroll state of the HTML linearization area
254: */
255: Rectangle recHtml = new Rectangle();
256: /**
257: * To store the scroll state of the pure text linearization area
258: */
259: int scrollText = 0;
260: /**
261: * To store the scroll state of the HTML linearization area
262: */
263: int scrollHtml = 0;
264:
265: public String toString() {
266: return getText();
267: }
268: }
|