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.IOException;
019: import java.io.Writer;
020: import java.util.Iterator;
021:
022: import de.uka.ilkd.key.logic.LocationDescriptor;
023: import de.uka.ilkd.key.logic.op.*;
024: import de.uka.ilkd.key.pp.LogicPrinter;
025: import de.uka.ilkd.key.pp.NotationInfo;
026: import de.uka.ilkd.key.pp.ProgramPrinter;
027: import de.uka.ilkd.key.rule.*;
028: import de.uka.ilkd.key.rule.export.*;
029:
030: public class HTMLFileTaclet extends HTMLFile {
031:
032: private ListOfTacletModelInfo tacletInfos;
033:
034: public HTMLFileTaclet(HTMLModel htmlModel,
035: HTMLContainer htmlContainer, ListOfTacletModelInfo tinfos,
036: int num) {
037: super (htmlModel, htmlContainer, "taclets" + num + ".html");
038: tacletInfos = tinfos;
039: }
040:
041: protected String getTitle() {
042: return "Taclets details";
043: }
044:
045: protected String getShortTitle() {
046: return getTitle();
047: }
048:
049: public void init(RuleExportModel model) {
050: super .init(model);
051:
052: IteratorOfTacletModelInfo it = tacletInfos.iterator();
053: while (it.hasNext()) {
054: final TacletModelInfo tacletInfo = it.next();
055: getFragmentAnchor(tacletInfo);
056: }
057: }
058:
059: protected void write(Writer w) throws IOException {
060: StringBuffer out = new StringBuffer();
061:
062: writeHeader(out);
063:
064: writeTopAnchor(out);
065:
066: writeNavBar(out);
067:
068: writeTacletDetails(out);
069:
070: writeFooter(out);
071:
072: w.write(out.toString());
073: }
074:
075: private void writeTacletDetails(StringBuffer out) {
076: IteratorOfTacletModelInfo it = tacletInfos.iterator();
077: while (it.hasNext()) {
078: final TacletModelInfo tacletInfo = it.next();
079: writeTacletDetails(out, tacletInfo);
080: }
081: }
082:
083: private void writeTacletDetails(StringBuffer out,
084: TacletModelInfo tinfo) {
085: final HTMLAnchor anchor = getFragmentAnchor(tinfo);
086:
087: // header
088: out.append("<!-- rule details -->\n");
089: out.append("<div class=\"rule\" id=\"" + anchor + "\">\n<h2>"
090: + tinfo.name() + "</h2>\n");
091: out.append("<dl>\n");
092:
093: // display name
094: out.append("<dt>display name</dt><dd>");
095: writeDisplayNameLink(out, tinfo.getDisplayName());
096: out.append("</dd>\n");
097:
098: // helpstring
099: final String helpText = tinfo.getTaclet().helpText();
100: if (helpText != null && !helpText.equals("")) {
101: out.append("<dt>help text</dt><dd>");
102: out.append(helpText);
103: out.append("</dd>\n");
104: }
105:
106: // options
107: if (tinfo.getOptions().size() > 0) {
108: out.append("<dt>options</dt><dd>");
109: writeTacletOptions(out, tinfo);
110: out.append("</dd>\n");
111: }
112:
113: // kind
114: String kind = getRuleKind(tinfo);
115: out.append("<dt>kind</dt><dd>" + kind + "</dd>\n");
116:
117: // rule sets
118: out.append("<dt>contained in</dt><dd>");
119: writeTacletRuleSets(out, tinfo);
120: out.append("</dd>\n");
121:
122: // introduced by
123: final TacletModelInfo introducer = tinfo.getIntroducingTaclet();
124: if (introducer != null) {
125: out.append("<dt>introduced by</dt><dd>");
126: writeTacletLink(out, introducer);
127: out.append("</dd>\n");
128: }
129:
130: // filename
131: out.append("<dt>source file</dt><dd>" + tinfo.getFilename()
132: + "</dd>\n");
133:
134: // footer
135: out.append("</dl>\n");
136: out.append("</div>\n\n");
137:
138: writeTacletDefinition(out, tinfo);
139:
140: writeTopLink(out);
141: }
142:
143: private void writeTacletRuleSets(StringBuffer out, TacletModelInfo t) {
144: final ListOfRuleSetModelInfo ruleSets = t.getRuleSets();
145: if (ruleSets.isEmpty()) {
146: out.append("none");
147: } else {
148: boolean first = true;
149: final IteratorOfRuleSetModelInfo it = ruleSets.iterator();
150: while (it.hasNext()) {
151: final RuleSetModelInfo ruleSet = it.next();
152: if (!first) {
153: out.append(", ");
154: }
155: writeRuleSetLink(out, ruleSet);
156: first = false;
157: }
158: }
159: }
160:
161: private String getRuleKind(TacletModelInfo tinfo) {
162: final Taclet t = tinfo.getTaclet();
163: String kind;
164: if (t instanceof NoFindTaclet) {
165: kind = "NoFindTaclet";
166: } else if (t instanceof RewriteTaclet) {
167: kind = "RewriteTaclet";
168: } else if (t instanceof AntecTaclet) {
169: kind = "AntecTaclet";
170: } else if (t instanceof SuccTaclet) {
171: kind = "SuccTaclet";
172: } else {
173: kind = "unknown (" + t.getClass().getName() + ")";
174: }
175: return kind;
176: }
177:
178: private void writeTacletDefinition(StringBuffer out,
179: TacletModelInfo tinfo) {
180: final Taclet t = tinfo.getTaclet();
181: // write schemavariable declarations
182: writeTacletSchemaVariables(out, t);
183:
184: // write pretty-printed taclet definition
185: LogicPrinter lp = new LogicPrinter(new ProgramPrinter(),
186: new NotationInfo(), null, true);
187: lp.printTaclet(t);
188: out.append("<pre>\n");
189: appendEscaped(out, lp.result());
190: out.append("</pre>\n");
191: }
192:
193: public static void writeTacletSchemaVariables(StringBuffer out,
194: final Taclet t) {
195: out.append("<pre>\n");
196: writeTacletSchemaVariablesHelper(out, t);
197: out.append("</pre>\n");
198: }
199:
200: public static void writeTacletSchemaVariablesHelper(
201: StringBuffer out, final Taclet t) {
202: SetOfSchemaVariable schemaVars = t.getIfFindVariables();
203: ListOfNewVarcond lnew = t.varsNew();
204: while (!lnew.isEmpty()) {
205: schemaVars = schemaVars
206: .add(lnew.head().getSchemaVariable());
207: lnew = lnew.tail();
208: }
209: IteratorOfNewDependingOn newDepIt = t.varsNewDependingOn();
210: while (newDepIt.hasNext()) {
211: schemaVars = schemaVars.add(newDepIt.next().first());
212: }
213:
214: if (schemaVars.size() > 0) {
215: out.append("\\schemaVariables {\n");
216: final IteratorOfSchemaVariable it = schemaVars.iterator();
217: while (it.hasNext()) {
218: final SchemaVariable schemaVar = it.next();
219: // write indentation
220: out.append(" ");
221: // write declaration
222: writeTacletSchemaVariable(out, schemaVar);
223: // write newline
224: out.append(";\n");
225: }
226: out.append("}\n");
227: }
228: }
229:
230: private static void writeSVModifiers(StringBuffer out,
231: SchemaVariable sv) {
232: boolean started = false;
233: if (sv.isRigid() && !sv.isVariableSV()) {
234: if (!started)
235: out.append("[");
236: out.append("rigid");
237: started = true;
238: }
239: if (sv.isListSV()) {
240: if (!started)
241: out.append("[");
242: else {
243: out.append(", ");
244: }
245: out.append("list");
246: started = true;
247: }
248:
249: if (started)
250: out.append("]");
251: }
252:
253: public static void writeTacletSchemaVariable(StringBuffer out,
254: SchemaVariable schemaVar) {
255: if (schemaVar.isOperatorSV()) {
256: final OperatorSV modalOpSV = (OperatorSV) schemaVar;
257: final Iterator it = modalOpSV.operators().iterator();
258: if (modalOpSV instanceof ModalOperatorSV) {
259: out.append("\\modalOperator { ");
260: } else {
261: out.append("\\operator");
262: }
263: String sep = "";
264: while (it.hasNext()) {
265: final Operator op = (Operator) it.next();
266: out.append(sep);
267: out.append(op.name());
268: sep = ", ";
269: }
270: out.append(" } " + modalOpSV.name());
271: } else if (schemaVar instanceof ListSV) {
272: if (schemaVar.matchType() == Function.class) {
273: out.append("\\function");
274: } else if (schemaVar.matchType() == LocationDescriptor.class) {
275: out.append("\\location");
276: } else {
277: out.append("(unknown)" + schemaVar.getClass());
278: }
279: writeSVModifiers(out, schemaVar);
280: out.append(" " + schemaVar.name());
281: } else if (schemaVar instanceof SortedSchemaVariable) {
282: final SortedSchemaVariable sortedSV = (SortedSchemaVariable) schemaVar;
283:
284: if (sortedSV.isTermSV()) {
285: out.append("\\term");
286: } else if (sortedSV.isFormulaSV()) {
287: out.append("\\formula");
288: } else if (sortedSV.isProgramSV()) {
289: out.append("\\program");
290: } else if (sortedSV.isVariableSV()) {
291: out.append("\\variables");
292: } else if (sortedSV.isSkolemTermSV()) {
293: out.append("\\skolemTerm");
294: } else {
295: out.append("?");
296: }
297: writeSVModifiers(out, schemaVar);
298: if (!schemaVar.isFormulaSV()) {
299: out.append(" " + sortedSV.sort());
300: }
301: out.append(" " + sortedSV.name());
302: } else if (schemaVar instanceof NameSV) {
303: out.append("?");
304: writeSVModifiers(out, schemaVar);
305: out.append(" " + schemaVar.name());
306: System.err
307: .println("NameSV in rule file? "
308: + "Please adapt HTMLFileTaclet#writeTacletSchemaVariable");
309: } else {
310: out.append("?");
311: writeSVModifiers(out, schemaVar);
312: out.append(" " + schemaVar.name());
313: System.err.println("Unknown schemavariable type "
314: + schemaVar);
315: }
316:
317: }
318: }
|