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:
021: import de.uka.ilkd.key.rule.export.*;
022:
023: public class HTMLFileByRuleName extends HTMLFile {
024: public static final int TACLETS_PER_FILE = 10;
025:
026: public HTMLFileByRuleName(HTMLModel model,
027: HTMLContainer htmlContainer) {
028: super (model, htmlContainer, "byRuleName.html");
029: }
030:
031: protected String getTitle() {
032: return "Taclets by rule name";
033: }
034:
035: protected String getShortTitle() {
036: return "by rule name";
037: }
038:
039: public void write(Writer w) throws IOException {
040: StringBuffer out = new StringBuffer();
041:
042: writeHeader(out);
043:
044: writeTopAnchor(out);
045:
046: writeNavBar(out);
047:
048: writeTOC(out);
049:
050: writeFooter(out);
051:
052: w.write(out.toString());
053:
054: writeAllFiles();
055: }
056:
057: public void init(RuleExportModel model) {
058: super .init(model);
059:
060: final IteratorOfTacletModelInfo it = model.taclets();
061: int n = 0;
062: ListOfTacletModelInfo list = SLListOfTacletModelInfo.EMPTY_LIST;
063: while (it.hasNext()) {
064: final TacletModelInfo t = it.next();
065: list = list.append(t);
066: n++;
067: if (n % TACLETS_PER_FILE == 0) {
068: HTMLFile file = new HTMLFileTaclet(htmlModel(), this ,
069: list, n / TACLETS_PER_FILE);
070: list = SLListOfTacletModelInfo.EMPTY_LIST;
071: }
072: }
073: if (!list.isEmpty()) {
074: HTMLFile file = new HTMLFileTaclet(htmlModel(), this , list,
075: n / TACLETS_PER_FILE + 1);
076: }
077:
078: initAllFiles(model);
079: }
080:
081: private void writeTOC(StringBuffer out) {
082: // TOC header
083: out.append("<!-- table of contents -->\n");
084: out.append("<div class=\"contents\">\n<h2>Rules</h2>\n");
085: if (model.getTaclets().size() == 1) {
086: out.append("There is 1 rule.\n");
087: } else {
088: out.append("There are " + model.getTaclets().size()
089: + " rules.\n");
090: }
091: out.append("<ol>\n");
092:
093: final IteratorOfTacletModelInfo it = model.taclets();
094: while (it.hasNext()) {
095: // TOC entry
096: final TacletModelInfo t = it.next();
097:
098: out.append("<li>");
099: writeTacletLink(out, t, true);
100: out.append("</li>\n");
101: }
102:
103: // TOC footer
104: out.append("</ol>\n</div>\n\n");
105:
106: writeTopLink(out);
107: }
108:
109: }
|