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 HTMLFileByDisplayName extends HTMLFile {
024: public HTMLFileByDisplayName(HTMLModel htmlModel,
025: HTMLContainer htmlContainer) {
026: super (htmlModel, htmlContainer, "byDisplayName.html");
027: }
028:
029: protected String getTitle() {
030: return "Taclets by display name";
031: }
032:
033: protected String getShortTitle() {
034: return "by display name";
035: }
036:
037: protected void init(RuleExportModel model) {
038: super .init(model);
039:
040: final IteratorOfDisplayNameModelInfo it = model.displayNames();
041: while (it.hasNext()) {
042: final DisplayNameModelInfo dn = it.next();
043: getFragmentAnchor(dn);
044: }
045: }
046:
047: protected void write(Writer w) throws IOException {
048: final StringBuffer out = new StringBuffer();
049:
050: writeHeader(out);
051: writeTopAnchor(out);
052: writeNavBar(out);
053: writeTOC(out);
054: writeDisplayNames(out);
055: writeFooter(out);
056:
057: w.write(out.toString());
058: }
059:
060: private void writeTOC(StringBuffer out) {
061: // TOC header
062: out.append("<!-- table of contents -->\n");
063: out
064: .append("<div class=\"contents\">\n<h2>Display names</h2>\n");
065: if (model.getDisplayNames().size() == 1) {
066: out.append("There is 1 unique display name.\n");
067: } else {
068: out.append("There are " + model.getDisplayNames().size()
069: + " unique display names.\n");
070: }
071: out.append("<ol>\n");
072:
073: final IteratorOfDisplayNameModelInfo it = model.displayNames();
074: while (it.hasNext()) {
075: // TOC entry
076: final DisplayNameModelInfo dn = it.next();
077:
078: final ListOfTacletModelInfo taclets = dn.getTaclets();
079: int tacletCount = taclets.size();
080:
081: out.append("<li>");
082: writeDisplayNameLink(out, dn);
083: if (tacletCount > 1) {
084: out.append(" (" + tacletCount + " rules");
085: String differences = getDifferences(taclets);
086: if (!"".equals(differences)) {
087: out.append(differences);
088: }
089: out.append(")");
090: }
091: out.append("</li>\n");
092: }
093:
094: // TOC footer
095: out.append("</ol>\n</div>\n\n");
096: }
097:
098: private String getDifferences(ListOfTacletModelInfo taclets) {
099: TacletModelInfo t0 = taclets.head();
100: final IteratorOfTacletModelInfo it = taclets.tail().iterator();
101: boolean differentOptions = false;
102: boolean differentIntroducer = false;
103: while (it.hasNext()) {
104: final TacletModelInfo t = it.next();
105: if (!t0.name().equals(t.name())) {
106: return "";
107: }
108: if (t0.getIntroducingTaclet() != t.getIntroducingTaclet()) {
109: differentIntroducer = true;
110: } else {
111: // assume different options
112: differentOptions = true;
113: }
114: }
115: String rv = "";
116: if (differentIntroducer) {
117: rv = rv + ", different introducer";
118: }
119: if (differentOptions) {
120: rv = rv + ", different options";
121: }
122: return rv;
123: }
124:
125: private void writeDisplayNames(StringBuffer out) {
126: writeTopLink(out);
127: final IteratorOfDisplayNameModelInfo it = model.displayNames();
128: while (it.hasNext()) {
129: final DisplayNameModelInfo dn = it.next();
130:
131: writeDisplayNameDetails(out, dn);
132:
133: writeTopLink(out);
134: }
135: }
136:
137: private void writeDisplayNameDetails(StringBuffer out,
138: final DisplayNameModelInfo dn) {
139: final HTMLAnchor anchor = getFragmentAnchor(dn);
140:
141: // header
142: out.append("<!-- display name details -->\n");
143: out.append("<div class=\"displayname\" id=\"" + anchor
144: + "\">\n");
145: out.append("<h2>" + dn + "</h2>\n");
146:
147: final ListOfTacletModelInfo taclets = dn.getTaclets();
148: if (taclets.size() == 1) {
149: out.append("There is 1 taclet with this display name.\n");
150: } else {
151: out.append("There are " + taclets.size()
152: + " taclets with this display name.\n");
153: }
154: out.append("<ol>\n");
155:
156: final IteratorOfTacletModelInfo it = taclets.iterator();
157: while (it.hasNext()) {
158: final TacletModelInfo t = it.next();
159:
160: out.append("<li>");
161: writeTacletLink(out, t, true);
162: out.append("</li>\n");
163: }
164:
165: out.append("</ol>\n");
166:
167: // footer
168: out.append("</div>\n");
169: }
170: }
|