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.Arrays;
021: import java.util.Comparator;
022:
023: import de.uka.ilkd.key.rule.export.*;
024:
025: public class HTMLFileByOption extends HTMLFile {
026:
027: private OptionModelInfo[][] options;
028: private ListOfCategoryModelInfo categories;
029: private int numCombinations;
030: private int[] strides;
031: private int[] numActives;
032:
033: public HTMLFileByOption(HTMLModel htmlModel,
034: HTMLContainer htmlContainer) {
035: super (htmlModel, htmlContainer, "byOption.html");
036: }
037:
038: protected String getTitle() {
039: return "Taclets by option";
040: }
041:
042: protected String getShortTitle() {
043: return "by option";
044: }
045:
046: public void init(RuleExportModel model) {
047: super .init(model);
048:
049: final IteratorOfOptionModelInfo it = model.options();
050: while (it.hasNext()) {
051: getFragmentAnchor(it.next());
052: }
053: }
054:
055: protected void write(Writer w) throws IOException {
056: StringBuffer out = new StringBuffer();
057:
058: writeHeader(out);
059:
060: writeTopAnchor(out);
061:
062: writeNavBar(out);
063:
064: writeTOC(out);
065:
066: writeChoiceTable(out);
067:
068: writeOptions(out);
069:
070: writeFooter(out);
071:
072: w.write(out.toString());
073: }
074:
075: private void writeTOC(StringBuffer out) {
076: // TOC header
077: out.append("<!-- table of contents -->\n");
078: out.append("<div class=\"contents\">\n<h2>Options</h2>\n");
079: int numChoices = model.getOptions().size();
080: if (numChoices == 1) {
081: out.append("There is 1 option");
082: } else {
083: out.append("There are " + numChoices + " options");
084: }
085: int numCategories = model.getCategories().size();
086: if (numCategories == 1) {
087: out.append(" in 1 category.\n");
088: } else {
089: out.append(" in " + numCategories + " categories.\n");
090: }
091:
092: out.append("<ul>\n");
093:
094: final IteratorOfCategoryModelInfo it = model.categories();
095: while (it.hasNext()) {
096: final CategoryModelInfo cat = it.next();
097: out.append("<li>" + cat + "\n");
098: out.append("<ol>\n");
099:
100: final IteratorOfOptionModelInfo it2 = cat.getOptions()
101: .iterator();
102: while (it2.hasNext()) {
103: final OptionModelInfo opt = it2.next();
104: final HTMLLink link = getFragmentLink(opt);
105: out.append("<li>" + link.toTag(opt.name()) + "</li>\n");
106: }
107:
108: out.append("</ol>\n");
109: out.append("</li>\n");
110: }
111:
112: // TOC footer
113: out.append("</ul>\n</div>\n\n");
114: }
115:
116: private void writeOptions(StringBuffer out) {
117: writeTopLink(out);
118:
119: final IteratorOfOptionModelInfo it = model.options();
120: while (it.hasNext()) {
121: final OptionModelInfo opt = it.next();
122:
123: writeOptionDetails(out, opt);
124:
125: writeTopLink(out);
126: }
127: }
128:
129: private void writeOptionDetails(StringBuffer out,
130: OptionModelInfo opt) {
131: final HTMLAnchor anchor = getFragmentAnchor(opt);
132:
133: // header
134: out.append("<!-- option details -->\n");
135: out.append("<div class=\"option\" id=\"" + anchor + "\">\n");
136: out.append("<h2>" + opt.name() + "</h2>\n");
137:
138: final ListOfTacletModelInfo taclets = opt.getTaclets();
139: if (taclets.size() == 1) {
140: out.append("There is 1 taclet belonging to this option.\n");
141: } else {
142: out.append("There are " + taclets.size()
143: + " taclets belonging to this option.\n");
144: }
145:
146: out.append("<dl>\n");
147:
148: // alternative choices
149: ListOfOptionModelInfo alternatives = opt.getCategory()
150: .getOptions().removeAll(opt);
151: out.append("<dt>alternatives</dt><dd>");
152: if (alternatives.size() == 0) {
153: out.append("none");
154: } else {
155: writeOptionList(out, alternatives);
156: }
157: out.append("</dd>\n");
158:
159: out.append("</dl>\n");
160:
161: out.append("<ol>\n");
162:
163: final IteratorOfTacletModelInfo it = taclets.iterator();
164: while (it.hasNext()) {
165: final TacletModelInfo t = it.next();
166:
167: out.append("<li>");
168: writeTacletLink(out, t, true);
169: out.append("</li>\n");
170: }
171:
172: out.append("</ol>\n");
173:
174: // footer
175: out.append("</div>\n");
176: }
177:
178: private ListOfCategoryModelInfo sortCategoriesByChoices(
179: ListOfCategoryModelInfo cats) {
180: CategoryModelInfo[] catArray = cats.toArray();
181: Arrays.sort(catArray, new Comparator() {
182: public int compare(Object a, Object b) {
183: return ((CategoryModelInfo) a).getOptions().size()
184: - ((CategoryModelInfo) b).getOptions().size();
185: }
186: });
187: return SLListOfCategoryModelInfo.EMPTY_LIST.prepend(catArray);
188: }
189:
190: private void writeChoiceTable(StringBuffer out) {
191: categories = sortCategoriesByChoices(model.getCategories());
192: final int numCategories = categories.size();
193: options = new OptionModelInfo[numCategories][];
194: int[] numChoices = new int[numCategories];
195: numCombinations = 1;
196: int n = 0;
197: out.append("<table border=\"1\">\n");
198: out.append("<caption>Number of active taclets</caption>\n");
199: out.append("<thead>\n<tr>\n");
200: final IteratorOfCategoryModelInfo it = categories.iterator();
201: while (it.hasNext()) {
202: final CategoryModelInfo cat = it.next();
203: options[n] = cat.getOptions().toArray();
204: numChoices[n] = options[n].length;
205: numCombinations *= numChoices[n];
206: out.append("<td>" + cat.name() + "</td>");
207: n++;
208: }
209:
210: strides = new int[numCategories];
211: int stride = 1;
212: for (n = numCategories - 1; n >= 0; n--) {
213: strides[n] = stride;
214: stride *= numChoices[n];
215: }
216:
217: numActives = new int[numCombinations];
218: out.append("<td align=\"right\">active taclets</td>");
219:
220: analyzeTaclets();
221:
222: out.append("</tr>\n</thead>\n");
223: out.append("<tbody>\n");
224:
225: writeChoiceTableBody(out);
226:
227: out.append("</tbody>\n");
228: out.append("</table>\n");
229: }
230:
231: private void analyzeTaclets() {
232: final IteratorOfTacletModelInfo it = model.taclets();
233: while (it.hasNext()) {
234: final TacletModelInfo t = it.next();
235: final ListOfOptionModelInfo optionList = t.getOptions();
236: analyzeTaclet(optionList, 0, 0);
237: }
238: }
239:
240: private void analyzeTaclet(ListOfOptionModelInfo list, int line,
241: int dim) {
242: if (dim == options.length) {
243: numActives[line] += 1;
244: return;
245: }
246:
247: final int stride = strides[dim];
248: OptionModelInfo[] choiceArray = options[dim];
249: for (int n = 0; n < choiceArray.length; n++) {
250: if (list.contains(choiceArray[n])) {
251: analyzeTaclet(list, line + stride * n, dim + 1);
252: // there's at most one option from any category
253: return;
254: }
255: }
256: // no option from this category, so add to all
257: for (int n = 0; n < choiceArray.length; n++) {
258: analyzeTaclet(list, line + stride * n, dim + 1);
259: }
260: }
261:
262: private void writeChoiceTableBody(StringBuffer out) {
263: for (int line = 0; line < numCombinations; line++) {
264: out.append("<tr>");
265: writeChoiceTableRow(out, line, 0);
266: out.append("</tr>\n");
267: }
268: }
269:
270: private void writeChoiceTableRow(StringBuffer out, int line, int dim) {
271: if (dim == options.length) {
272: out.append("<td align=\"right\">" + numActives[line]
273: + "</td>");
274: return;
275: }
276:
277: //System.out.println("line: "+line+", dim: "+dim);
278:
279: final int stride = strides[dim];
280: if (line % stride == 0) {
281: final OptionModelInfo opt = options[dim][(line / stride)
282: % options[dim].length];
283: final String name = opt.name().toString();
284: final int posColon = name.indexOf(':');
285: final String shortName = name.substring(posColon + 1);
286:
287: out.append("<td rowspan=\"" + stride + "\">" + shortName
288: + "</td>");
289: }
290: writeChoiceTableRow(out, line, dim + 1);
291: }
292: }
|