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: //This file is part of KeY - Integrated Deductive Software Design
009: //Copyright (C) 2001-2003 Universitaet Karlsruhe, Germany
010: // and Chalmers University of Technology, Sweden
011: //
012: //The KeY system is protected by the GNU General Public License.
013: //See LICENSE.TXT for details.
014: //
015:
016: package de.uka.ilkd.key.rule.export.html;
017:
018: import java.io.*;
019: import java.net.URL;
020: import java.text.SimpleDateFormat;
021: import java.util.Date;
022: import java.util.HashMap;
023: import java.util.Iterator;
024: import java.util.zip.GZIPOutputStream;
025:
026: import de.uka.ilkd.key.gui.Main;
027: import de.uka.ilkd.key.rule.export.*;
028: import de.uka.ilkd.key.util.KeYResourceManager;
029:
030: public abstract class HTMLFile extends HTMLContainer {
031:
032: private static final String PRCSVERSION = Main.INTERNAL_VERSION;
033:
034: static KeYResourceManager resManager = KeYResourceManager
035: .getManager();
036:
037: public static String getTemplate(String s) {
038: //System.out.println("load template: "+s);
039: URL templateURL = resManager.getResourceFile(HTMLFile.class, s);
040: if (templateURL == null) {
041: //System.out.println("could not get resource URL");
042: return null;
043: }
044: //System.out.println("resource URL is:"+templateURL);
045: char[] readBuffer = new char[1024];
046: StringBuffer textBuffer = new StringBuffer();
047: try {
048: FileReader reader = new FileReader(templateURL.getFile());
049: int read;
050: while ((read = reader.read(readBuffer)) > 0) {
051: textBuffer.append(readBuffer, 0, read);
052: }
053: } catch (FileNotFoundException e) {
054: System.err.println("file not found: " + templateURL);
055: return null;
056: } catch (IOException e) {
057: System.err.println("could not read from file: "
058: + templateURL);
059: return null;
060: }
061: return textBuffer.toString();
062: }
063:
064: private HTMLModel htmlModel;
065: private HTMLContainer htmlContainer;
066: private String filename;
067: private int idCount = 0;
068:
069: private HashMap fragment2id = new HashMap();
070:
071: protected RuleExportModel model = null;
072:
073: public HTMLFile(HTMLModel htmlModel, HTMLContainer htmlContainer,
074: String filename) {
075: super (htmlContainer.getRootFolder());
076: this .htmlModel = htmlModel;
077: this .htmlContainer = htmlContainer;
078: this .filename = filename;
079:
080: htmlContainer.addFile(this );
081: }
082:
083: protected HTMLModel htmlModel() {
084: return htmlModel;
085: }
086:
087: protected HTMLContainer htmlContainer() {
088: return htmlContainer;
089: }
090:
091: public String getFilename() {
092: return filename;
093: }
094:
095: public String getRelPath(HTMLFile targetFile) {
096: return htmlModel.getRelPath(this , targetFile);
097: }
098:
099: public String getNextId() {
100: idCount++;
101: return "id" + idCount;
102: }
103:
104: public HTMLLink getFileLink(HTMLFile target) {
105: return htmlModel.getFileLink(this , target);
106: }
107:
108: public HTMLLink getFragmentLink(Object key) {
109: return htmlModel.getFragmentLink(this , key);
110: }
111:
112: public HTMLAnchor getFragmentAnchor(Object key) {
113: return htmlModel.getFragmentAnchor(this , key);
114: }
115:
116: public void addFragment(HTMLFragment fragment, String id) {
117: fragment2id.put(fragment, id);
118: }
119:
120: public String getFragmentId(HTMLFragment fragment) {
121: return (String) fragment2id.get(fragment);
122: }
123:
124: public String toString() {
125: return "HTMLFile with filename " + filename;
126: }
127:
128: protected static String TOPANCHOR = "<!-- top anchor -->\n"
129: + "<div id=\"top\"></div>\n\n";
130: protected static String TOPLINK = "<!-- top link -->\n"
131: + "<hr /><div class=\"navtop\">"
132: + "<a href=\"#top\">Top</a></div>\n\n";
133:
134: protected void writeTopAnchor(StringBuffer out) {
135: out.append(TOPANCHOR);
136: }
137:
138: protected void writeTopLink(StringBuffer out) {
139: out.append(TOPLINK);
140: }
141:
142: protected void writeNavBar(StringBuffer out) {
143: out.append("<!-- navigation bar -->\n");
144: out.append("<div class=\"nav\">\n");
145:
146: //out.append ( "<span class=\"navitem\"><a href=\"index.html\">main page</a></span>\n" );
147:
148: boolean first = true;
149: final Iterator it = htmlModel.files();
150: while (it.hasNext()) {
151: HTMLFile file = (HTMLFile) it.next();
152: if (!first) {
153: out.append(" | ");
154: }
155: out.append("<span class=\"navitem\">");
156: if (file == this ) {
157: out.append(getShortTitle());
158: } else {
159: out.append("<a href=\"" + file.getFilename() + "\">"
160: + file.getShortTitle() + "</a>");
161: }
162: out.append("</span>");
163: first = false;
164: }
165:
166: out.append("</div>\n\n");
167: }
168:
169: protected void writeHeader(StringBuffer out) {
170: out
171: .append("<?xml version=\"1.0\" encoding=\"utf-8\"?>\n"
172: + "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.1//EN\" \"http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd\">\n"
173: + "<html xmlns=\"http://www.w3.org/1999/xhtml\" xml:lang=\"en\">\n"
174: + "\n"
175: + "<head>\n"
176: + "<title>"
177: + getTitle()
178: + "</title>\n"
179: + "<link rel=\"stylesheet\" href=\"style.css\" type=\"text/css\" />\n"
180: + "</head>" + "\n" + "<body>\n");
181: }
182:
183: /** returns name displayed in title bar */
184: protected abstract String getTitle();
185:
186: /** returns name displayed in navigation bar */
187: protected abstract String getShortTitle();
188:
189: protected void writeFooter(StringBuffer out) {
190: out.append("<div class=\"versioninfo\">");
191: out.append("<p>Generated from internal version " + PRCSVERSION
192: + " on " + formatDate() + ".</p>");
193: out.append("</div>");
194: out.append("</body>\n\n</html>\n");
195: }
196:
197: private String formatDate() {
198: Date now = new Date();
199: SimpleDateFormat formatter = new SimpleDateFormat(
200: "yyyy-MM-dd HH:mm z");
201: return formatter.format(now);
202: }
203:
204: public void write() {
205: try {
206: OutputStreamWriter writer = null;
207: if (false /* useGZIP */) {
208: FileOutputStream fos = new FileOutputStream(htmlModel
209: .getRootFolder()
210: + getFilename() + ".gz");
211: GZIPOutputStream gos = new GZIPOutputStream(fos);
212: writer = new OutputStreamWriter(gos);
213: } else {
214: FileOutputStream fos = new FileOutputStream(htmlModel
215: .getRootFolder()
216: + getFilename());
217: writer = new OutputStreamWriter(fos);
218: }
219: write(writer);
220: writer.close();
221: } catch (IOException e) {
222: System.err.println(e);
223: }
224: }
225:
226: protected abstract void write(Writer w) throws IOException;
227:
228: protected void init(RuleExportModel model) {
229: this .model = model;
230: //System.out.println("HTMLFile.init(), "+getFilename());
231: }
232:
233: protected void writeTacletLink(StringBuffer out, TacletModelInfo t) {
234: writeTacletLink(out, t, false);
235: }
236:
237: protected void writeTacletLink(StringBuffer out, TacletModelInfo t,
238: boolean longVersion) {
239: final HTMLLink link = getFragmentLink(t);
240: out.append(link.toTag(t.name()));
241: if (longVersion) {
242: if (t.getIntroducingTaclet() != null) {
243: out.append(" <");
244: writeTacletLink(out, t.getIntroducingTaclet());
245: out.append(">");
246: }
247: if (t.getOptions().size() > 0) {
248: out.append(" (");
249: writeTacletOptions(out, t);
250: out.append(")");
251: }
252: }
253: }
254:
255: protected void writeRuleSetLink(StringBuffer out,
256: RuleSetModelInfo rs) {
257: final HTMLLink link = getFragmentLink(rs);
258: out.append(link.toTag(escape(rs.name())));
259: }
260:
261: protected void writeDisplayNameLink(StringBuffer out,
262: DisplayNameModelInfo dn) {
263: final HTMLLink link = getFragmentLink(dn);
264: out.append(link.toTag(dn));
265: }
266:
267: protected void writeOptionLink(StringBuffer out, OptionModelInfo opt) {
268: final HTMLLink link = getFragmentLink(opt);
269: out.append(link.toTag(opt.name()));
270: }
271:
272: protected void writeTacletOptions(StringBuffer out,
273: TacletModelInfo t) {
274: final ListOfOptionModelInfo options = t.getOptions();
275:
276: writeOptionList(out, options);
277: }
278:
279: protected void writeOptionList(StringBuffer out,
280: ListOfOptionModelInfo options) {
281: final IteratorOfOptionModelInfo it = options.iterator();
282: boolean first = true;
283: while (it.hasNext()) {
284: final OptionModelInfo opt = it.next();
285: if (!first) {
286: out.append(", ");
287: }
288: writeOptionLink(out, opt);
289: first = false;
290: }
291: }
292:
293: protected StringBuffer appendEscaped(StringBuffer sb, Object o) {
294: return appendEscaped(sb, o.toString());
295: }
296:
297: protected StringBuffer appendEscaped(StringBuffer sb, String s) {
298: for (int n = 0; n < s.length(); n++) {
299: switch (s.charAt(n)) {
300: case '"':
301: sb.append(""");
302: break;
303: case '&':
304: sb.append("&");
305: break;
306: case '<':
307: sb.append("<");
308: break;
309: case '>':
310: sb.append(">");
311: break;
312: //case '\n':
313: // sb.append("<br />\n");
314: // break;
315: default:
316: sb.append(s.charAt(n));
317: }
318: }
319: return sb;
320: }
321:
322: protected String escape(Object o) {
323: StringBuffer sb = new StringBuffer();
324: appendEscaped(sb, o);
325: return sb.toString();
326: }
327: }
|