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 HTMLFileByRuleSet extends HTMLFile {
024:
025: public HTMLFileByRuleSet(HTMLModel model,
026: HTMLContainer htmlContainer) {
027: super (model, htmlContainer, "byRuleSet.html");
028: }
029:
030: protected String getTitle() {
031: return "Taclets by rule set";
032: }
033:
034: protected String getShortTitle() {
035: return "by rule set";
036: }
037:
038: public void init(RuleExportModel model) {
039: super .init(model);
040:
041: final IteratorOfRuleSetModelInfo it = model.ruleSets();
042: while (it.hasNext()) {
043: getFragmentAnchor(it.next());
044: }
045: }
046:
047: protected void write(Writer w) throws IOException {
048: StringBuffer out = new StringBuffer();
049:
050: writeHeader(out);
051:
052: writeTopAnchor(out);
053:
054: writeNavBar(out);
055:
056: writeTOC(out);
057:
058: writeRuleSets(out);
059:
060: writeFooter(out);
061:
062: w.write(out.toString());
063: }
064:
065: private void writeTOC(StringBuffer out) {
066: // TOC header
067: out.append("<!-- table of contents -->\n");
068: out.append("<div class=\"contents\">\n<h2>Rule sets</h2>\n");
069: if (model.getRuleSets().size() == 1) {
070: out.append("There is 1 rule set.\n");
071: } else {
072: out.append("There are " + model.getRuleSets().size()
073: + " rule sets.\n");
074: }
075: out.append("<ol>\n");
076:
077: final IteratorOfRuleSetModelInfo it = model.ruleSets();
078: while (it.hasNext()) {
079: // TOC entry
080: final RuleSetModelInfo rs = it.next();
081: final HTMLLink link = getFragmentLink(rs);
082:
083: out.append("<li>" + link.toTag(escape(rs.name()))
084: + "</li>\n");
085: }
086:
087: // TOC footer
088: out.append("</ol>\n</div>\n\n");
089: }
090:
091: private void writeRuleSets(StringBuffer out) {
092: writeTopLink(out);
093:
094: final IteratorOfRuleSetModelInfo it = model.ruleSets();
095: while (it.hasNext()) {
096: final RuleSetModelInfo rs = it.next();
097:
098: writeRuleSetDetails(out, rs);
099:
100: writeTopLink(out);
101: }
102: }
103:
104: private void writeRuleSetDetails(StringBuffer out,
105: final RuleSetModelInfo rs) {
106: final HTMLAnchor anchor = getFragmentAnchor(rs);
107:
108: // header
109: out.append("<!-- rule set details -->\n");
110: out.append("<div class=\"ruleset\" id=\"" + anchor + "\">\n");
111: out.append("<h2>Rule set <em>" + escape(rs.name())
112: + "</em></h2>\n");
113:
114: final ListOfTacletModelInfo localTacletList = rs.getTaclets();
115: final IteratorOfTacletModelInfo it = localTacletList.iterator();
116:
117: final ListOfRuleSetModelInfo intersectingSets = rs
118: .getIntersectingSets();
119: final ListOfRuleSetModelInfo super Sets = rs.getSuperSets();
120: final ListOfRuleSetModelInfo subSets = rs.getSubSets();
121: final ListOfRuleSetModelInfo equalSets = rs.getEqualSets();
122:
123: if (!intersectingSets.isEmpty() || !super Sets.isEmpty()
124: || !subSets.isEmpty() || !equalSets.isEmpty()) {
125: out.append("<dl>\n");
126:
127: // definition
128: if (rs.getDefinition() != null) {
129: out.append("<dt>definition</dt><dd>");
130: out.append(escape(rs.getDefinition()));
131: out.append("</dd>\n");
132: }
133:
134: // intersecting sets
135: if (!intersectingSets.isEmpty()) {
136: out.append("<dt>intersects with</dt><dd>");
137: writeRuleSetList(out, intersectingSets);
138: out.append("</dd>\n");
139: }
140:
141: // subsets
142: if (!subSets.isEmpty()) {
143: out.append("<dt>superset of</dt><dd>");
144: writeRuleSetList(out, subSets);
145: out.append("</dd>\n");
146: }
147:
148: // supersets
149: if (!super Sets.isEmpty()) {
150: out.append("<dt>subset of</dt><dd>");
151: writeRuleSetList(out, super Sets);
152: out.append("</dd>\n");
153: }
154:
155: // equal sets
156: if (!equalSets.isEmpty()) {
157: out.append("<dt>equal to</dt><dd>");
158: writeRuleSetList(out, equalSets);
159: out.append("</dd>\n");
160: }
161:
162: out.append("</dl>\n");
163: }
164:
165: // rule list header
166: if (localTacletList.size() == 1) {
167: out.append("There is 1 rule in this rule set.\n");
168: } else {
169: out.append("There are " + localTacletList.size()
170: + " rules in this rule set.\n");
171: }
172: out.append("<ol>\n");
173:
174: // rule list elements
175: while (it.hasNext()) {
176: final TacletModelInfo t = it.next();
177: out.append("<li>");
178: writeTacletLink(out, t, true);
179: out.append("</li>\n");
180: }
181:
182: // rule list footer
183: out.append("</ol>\n");
184:
185: // footer
186: out.append("</div>\n\n");
187: }
188:
189: private void writeRuleSetList(StringBuffer out,
190: ListOfRuleSetModelInfo ruleSets) {
191: if (ruleSets.isEmpty()) {
192: out.append("none");
193: } else {
194: boolean first = true;
195: final IteratorOfRuleSetModelInfo it = ruleSets.iterator();
196: while (it.hasNext()) {
197: final RuleSetModelInfo ruleSet = it.next();
198: if (!first) {
199: out.append(", ");
200: }
201: writeRuleSetLink(out, ruleSet);
202: first = false;
203: }
204: }
205: }
206: }
|