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.util.keydoc.html;
009:
010: import java.io.DataInputStream;
011: import java.io.File;
012: import java.io.FileInputStream;
013: import java.io.IOException;
014: import de.uka.ilkd.key.util.keydoc.parser.*;
015:
016: import antlr.CommonAST;
017:
018: /**
019: * This class is my impelementation of the builder itself.
020: * It builds the HTML documentation file of a given .key file.
021: * To parse the .key file it uses classes generated by the Tool antlr.
022: * The location of the parsing package is src.parser.
023: * It stores the HTML file and certain information needed by the director
024: * (name of the file, shordescription of the file)
025: * in a BoxedFile.
026: *
027: * @author sebastian
028: *
029: */
030: class KDKeYToHTMLBuilder extends KeYToHTMLBuilder {
031:
032: final static String bgcolor = "#BEBEFF"; // The Backgroundcolor of the HTML table headlines
033:
034: protected static BoxedFile buildHTMLFile(File toBuild) {
035: try {
036:
037: StringBuffer html = new StringBuffer(40);
038:
039: // firing up the lexer, parser and treewalker
040: FileInputStream file = new FileInputStream(toBuild);
041: DataInputStream dataInput = new DataInputStream(file);
042: KeYDocLexer lexer = new KeYDocLexer(dataInput);
043: KeYDocParser parser = new KeYDocParser(lexer);
044: parser.startRule();
045: CommonAST parseTree = (CommonAST) parser.getAST();
046: KeYDocTreeWalker walker = new KeYDocTreeWalker();
047: walker.keyDocExpr(parseTree);
048:
049: // htmlcode generation
050:
051: // the header
052: html.append("<html><head><title>");
053: html.append(toBuild.getName());
054: html.append("</title></head>");
055:
056: // the body
057: html.append("<body>");
058:
059: html.append("<center><b>");
060: html.append(toBuild.getName());
061: html.append("</b></center>");
062: // provable??
063: if (walker.provable != null) {
064: html.append("<dl><dt><b>Provable:</b></dt><dd>");
065: html.append(walker.provable);
066: html.append("</dd></dl>");
067: }
068:
069: // Integers for the determination of the first line of text.
070: int firstOffset = html.length();
071: int firstLength = parser.firstLength;
072: int firstLinkLength = 0;
073:
074: // htmlText. First LinkTags are inserted
075: StringBuffer htmlText = parser.htmlText;
076: int position; // position of the Linktags
077:
078: int linkOffset = 0; // Adds length of the linktags themselfes to the length of the text.
079: for (int i = 0; i < parser.links.size(); i++) {
080: position = ((Integer) parser.links.get(i)).intValue();
081: String link = ((StringBuffer) walker.link.get(i))
082: .toString();
083: htmlText.insert(position + linkOffset, link);
084: linkOffset += link.length();
085: if (position < firstLength)
086: firstLinkLength += link.length();
087: // pretty complicated lines short: copy the LinkTags into the htmlText StringBuffer.
088: // update the length of the firstline, if the Linktag is within it.
089: }
090: firstLength += firstLinkLength;
091:
092: html.append(htmlText);
093:
094: // see??
095: if (walker.see.size() != 0) {
096:
097: html.append("<dl><dt><b>See</b></dt><dd><code>");
098: html.append(walker.see.get(0));
099: for (int i = 1; i < walker.see.size(); i++) {
100: html.append(", ");
101: html.append(walker.see.get(i));
102: }
103: html.append("</code></dd></dl>");
104: }
105:
106: html.append("<hr>");
107:
108: html.append("<pre>");
109: html.append(parser.keyText);
110: html.append("</pre>");
111:
112: html.append("<hr>");
113:
114: // statistics??
115: if (walker.stat1.size() != 0) {
116: html
117: .append("<center><table border=\"1\" width=\"80%\"><colgroup><col width=\"2*\"><col width=\"1*\"></colgroup><tr><td colspan=\"1\" bgcolor=\""
118: + bgcolor
119: + "\"><h2>Statistics</h2></td><td colspan=\"1\" bgcolor=\""
120: + bgcolor + "\"> </td></tr>");
121: for (int i = 0; i < walker.stat1.size(); i++) {
122: html
123: .append("<tr><code><td class=\"left\" valign=\"top\"><code>");
124: html.append(walker.stat1.get(i));
125: html.append("</td><td class=\"right\">");
126: html.append(walker.stat2.get(i));
127: html.append("</td></code></tr>");
128: }
129: html.append("</table></center><br>");
130: }
131:
132: html.append("<table border=\"0\" cellspacing=\"40\"><tr>");
133:
134: // Since??
135: if (walker.since != null) {
136: html.append("<td><dl><dt><b>Since:</b></dt><dd><code>");
137: html.append(walker.since);
138: html.append("</code></dd></dl></td>");
139: }
140:
141: // Version??
142: if (walker.version != null) {
143: html
144: .append("<td><dl><dt><b>Version:</b></dt><dd><code>");
145: html.append(walker.version);
146: html.append("</code></dd></dl></td>");
147: }
148:
149: // Author??
150: if (walker.auth.size() != 0) {
151: html.append("<td><dl><dt><b>Author</b></dt><dd><code>");
152: html.append(walker.auth.get(0));
153: for (int i = 1; i < walker.auth.size(); i++) {
154: html.append(", ");
155: html.append(walker.auth.get(i));
156: }
157: html.append("</code></dd></dl></td>");
158: }
159:
160: // Deprecated??
161: if (walker.deprecated != false) {
162: html
163: .append("<td><dl><dt><b>Deprecated</b></dt><dd><code>");
164: html.append("</code></dd></dl></td>");
165: }
166:
167: html.append("</tr></table>");
168:
169: // TODO: delete .key
170: return new BoxedFile(toBuild, firstLength, firstOffset,
171: new HTMLFile(html));
172:
173: } catch (IOException iOE) {
174: System.out
175: .println("IOException occured during parsing file");
176: } catch (Exception e) {
177: System.out.println("Exception: " + e
178: + " occured during parsing file");
179: }
180:
181: System.out.println("Due to the Error, file will be skipped.");
182: return null;
183: }
184:
185: }
|