Clover Coverage Report
Coverage timestamp: Sa Aug 2 2008 13:56:27 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
../../../../../../img/srcFileCovDistChart0.png 88% of files have more coverage
184   495   60   11,5
104   313   0,33   16
16     3,75  
1    
 
  Qedeq2Wiki       Line # 65 184 60 0% 0.0
 
No Tests
 
1    /* $Id: Qedeq2Wiki.java,v 1.1 2008/07/26 07:58:28 m31 Exp $
2    *
3    * This file is part of the project "Hilbert II" - http://www.qedeq.org
4    *
5    * Copyright 2000-2008, Michael Meyling <mime@qedeq.org>.
6    *
7    * "Hilbert II" is free software; you can redistribute
8    * it and/or modify it under the terms of the GNU General Public
9    * License as published by the Free Software Foundation; either
10    * version 2 of the License, or (at your option) any later version.
11    *
12    * This program is distributed in the hope that it will be useful,
13    * but WITHOUT ANY WARRANTY; without even the implied warranty of
14    * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15    * GNU General Public License for more details.
16    */
17   
18    package org.qedeq.kernel.bo.service.latex;
19   
20    import java.io.File;
21    import java.io.FileOutputStream;
22    import java.io.IOException;
23    import java.io.OutputStream;
24    import java.io.PrintStream;
25   
26    import org.qedeq.base.trace.Trace;
27    import org.qedeq.base.utility.StringUtility;
28    import org.qedeq.kernel.base.list.Element;
29    import org.qedeq.kernel.base.list.ElementList;
30    import org.qedeq.kernel.base.module.Axiom;
31    import org.qedeq.kernel.base.module.Chapter;
32    import org.qedeq.kernel.base.module.ChapterList;
33    import org.qedeq.kernel.base.module.FunctionDefinition;
34    import org.qedeq.kernel.base.module.Latex;
35    import org.qedeq.kernel.base.module.LatexList;
36    import org.qedeq.kernel.base.module.LiteratureItem;
37    import org.qedeq.kernel.base.module.LiteratureItemList;
38    import org.qedeq.kernel.base.module.Node;
39    import org.qedeq.kernel.base.module.NodeType;
40    import org.qedeq.kernel.base.module.PredicateDefinition;
41    import org.qedeq.kernel.base.module.Proposition;
42    import org.qedeq.kernel.base.module.Rule;
43    import org.qedeq.kernel.base.module.Section;
44    import org.qedeq.kernel.base.module.SectionList;
45    import org.qedeq.kernel.base.module.Subsection;
46    import org.qedeq.kernel.base.module.SubsectionList;
47    import org.qedeq.kernel.base.module.SubsectionType;
48    import org.qedeq.kernel.base.module.VariableList;
49    import org.qedeq.kernel.bo.QedeqBo;
50   
51   
52    /**
53    * Transfer a QEDEQ module into text files in MediaWiki format.
54    * <p>
55    * LATER mime 20060831: This is just a quick hacked generator. This class just
56    * generates some text files.
57    * <p>
58    * <b>It is not finished!</b>
59    * <p>
60    * It should be compared with Qedeq2Latex and then refactored to reuse common functions.
61    *
62    * @version $Revision: 1.1 $
63    * @author Michael Meyling
64    */
 
65    public class Qedeq2Wiki {
66   
67    /** This class. */
68    private static final Class CLASS = Qedeq2Wiki.class;
69   
70    /** Alphabet for tagging. */
71    private static final String ALPHABET = "abcdefghijklmnopqrstuvwxyz";
72   
73    /** QEDEQ module properties object to work on. */
74    private final QedeqBo prop;
75   
76    /** Output goes here. */
77    private PrintStream printer;
78   
79    /** Filter text to get and produce text in this language. */
80    private String language;
81   
82    /** Transformer to get LaTeX out of {@link Element}s. */
83    private final Element2Latex elementConverter;
84   
85    /** Destination directory. */
86    private File outputDirectory;
87   
88    /**
89    * Constructor.
90    *
91    * @param prop QEDEQ module properties object.
92    */
 
93  0 toggle public Qedeq2Wiki(final QedeqBo prop) {
94  0 this.prop = prop;
95  0 this.elementConverter = new Element2Latex((prop.hasLoadedRequiredModules()
96    ? prop.getRequiredModules() : null));
97    }
98   
99    /**
100    * Prints a LaTeX file into a given output stream.
101    *
102    * @param language Filter text to get and produce text in this language only.
103    * @param level Filter for this detail level. LATER mime 20050205: not supported
104    * yet.
105    * @param outputDirectory Write files to this directory.
106    * @throws IOException
107    */
 
108  0 toggle public final synchronized void printWiki(final String language, final String level,
109    final File outputDirectory) throws IOException {
110  0 if (language == null) {
111  0 this.language = "en";
112    } else {
113  0 this.language = language;
114    }
115  0 this.outputDirectory = outputDirectory;
116  0 printQedeqChapters();
117  0 printQedeqBibliography();
118  0 if (printer.checkError()) {
119  0 throw new IOException("TODO mime: better use another OutputStream");
120    }
121    }
122   
123    /**
124    * Print all chapters.
125    *
126    * @throws IOException Writing failed.
127    */
 
128  0 toggle private void printQedeqChapters() throws IOException {
129  0 final ChapterList chapters = prop.getQedeq().getChapterList();
130  0 for (int i = 0; i < chapters.size(); i++) {
131  0 final String label = prop.getQedeq().getHeader().getSpecification()
132    .getName() + "_ch_" + i;
133  0 final OutputStream outputStream = new FileOutputStream(new File(outputDirectory,
134    label + "_" + language + ".wiki"));
135  0 this.printer = new PrintStream(outputStream);
136  0 final Chapter chapter = chapters.get(i);
137  0 printer.print("\\chapter");
138  0 if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) {
139  0 printer.print("*");
140    }
141  0 printer.println("== " + getLatexListEntry(chapter.getTitle()) + " ==");
142  0 printer.println();
143  0 printer.println("<div id=\"" + label + "\"></div>");
144    // if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) {
145  0 printer.println();
146  0 if (chapter.getIntroduction() != null) {
147  0 printer.println(getLatexListEntry(chapter.getIntroduction()));
148  0 printer.println();
149    }
150  0 final SectionList sections = chapter.getSectionList();
151  0 if (sections != null) {
152  0 printSections(i, sections);
153  0 printer.println();
154    }
155  0 printer.println("%% end of chapter " + getLatexListEntry(chapter.getTitle()));
156  0 printer.println();
157    }
158    }
159   
160    /**
161    * Print bibliography (if any).
162    */
 
163  0 toggle private void printQedeqBibliography() {
164  0 final LiteratureItemList items = prop.getQedeq().getLiteratureItemList();
165  0 if (items == null) {
166  0 return;
167    }
168  0 printer.println("\\begin{thebibliography}{99}");
169  0 for (int i = 0; i < items.size(); i++) {
170  0 final LiteratureItem item = items.get(i);
171  0 printer.print("\\bibitem{" + item.getLabel() + "} ");
172  0 printer.println(getLatexListEntry(item.getItem()));
173  0 printer.println();
174    }
175  0 printer.println("\\end{thebibliography}");
176  0 printer.println("\\addcontentsline{toc}{chapter}{Literaturverzeichnis}");
177    }
178   
179    /**
180    * Print all given sections.
181    *
182    * @param chapter Chapter number.
183    * @param sections List of sections.
184    */
 
185  0 toggle private void printSections(final int chapter, final SectionList sections) {
186  0 if (sections == null) {
187  0 return;
188    }
189  0 for (int i = 0; i < sections.size(); i++) {
190  0 final Section section = sections.get(i);
191  0 printer.print("\\section{");
192  0 printer.print(getLatexListEntry(section.getTitle()));
193  0 final String label = "chapter" + chapter + "_section" + i;
194  0 printer.println("} \\label{" + label + "} \\hypertarget{" + label + "}{}");
195  0 printer.println(getLatexListEntry(section.getIntroduction()));
196  0 printer.println();
197  0 printSubsections(section.getSubsectionList());
198    }
199    }
200   
201    /**
202    * Print all given subsections.
203    *
204    * @param nodes List of subsections.
205    */
 
206  0 toggle private void printSubsections(final SubsectionList nodes) {
207  0 if (nodes == null) {
208  0 return;
209    }
210  0 for (int i = 0; i < nodes.size(); i++) {
211  0 final SubsectionType subsectionType = nodes.get(i);
212  0 if (subsectionType instanceof Node) {
213  0 final Node node = (Node) subsectionType;
214  0 printer.println(getLatexListEntry(node.getPrecedingText()));
215  0 printer.println();
216  0 printer.println("\\par");
217  0 final String id = node.getId();
218  0 final NodeType type = node.getNodeType();
219  0 String title = null;
220  0 if (node.getTitle() != null) {
221  0 title = getLatexListEntry(node.getTitle());
222    }
223  0 if (type instanceof Axiom) {
224  0 printAxiom((Axiom) type, title, id);
225  0 } else if (type instanceof PredicateDefinition) {
226  0 printPredicateDefinition((PredicateDefinition) type, title, id);
227  0 } else if (type instanceof FunctionDefinition) {
228  0 printFunctionDefinition((FunctionDefinition) type, title, id);
229  0 } else if (type instanceof Proposition) {
230  0 printProposition((Proposition) type, title, id);
231  0 } else if (type instanceof Rule) {
232  0 printRule((Rule) type, title, id);
233    } else {
234  0 throw new RuntimeException((type != null ? "unknown type: "
235    + type.getClass().getName() : "node type empty"));
236    }
237  0 printer.println();
238  0 printer.println(getLatexListEntry(node.getSucceedingText()));
239    } else {
240  0 final Subsection subsection = (Subsection) subsectionType;
241  0 if (subsection.getTitle() != null) {
242  0 printer.print("\\subsection{");
243  0 printer.println(getLatexListEntry(subsection.getTitle()));
244  0 printer.println("}");
245    }
246  0 printer.println(getLatexListEntry(subsection.getLatex()));
247    }
248  0 printer.println();
249  0 printer.println();
250    }
251    }
252   
253    /**
254    * Print axiom.
255    *
256    * @param axiom Print this.
257    * @param title Extra name.
258    * @param id Label for marking this axiom.
259    */
 
260  0 toggle private void printAxiom(final Axiom axiom, final String title, final String id) {
261  0 printer.println("\\begin{ax}" + (title != null ? "[" + title + "]" : ""));
262  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
263  0 printFormula(axiom.getFormula().getElement());
264  0 printer.println(getLatexListEntry(axiom.getDescription()));
265  0 printer.println("\\end{ax}");
266    }
267   
268    /**
269    * Print top level formula. If the formula has the form <code>AND(.., .., ..)</code> the
270    * formula is broken down in several labeled lines.
271    *
272    * @param element Formula to print.
273    * @param mainLabel Main formula label.
274    */
 
275  0 toggle private void printTopFormula(final Element element, final String mainLabel) {
276  0 if (!element.isList() || !element.getList().getOperator().equals("AND")) {
277  0 printFormula(element);
278  0 return;
279    }
280  0 final ElementList list = element.getList();
281  0 printer.println("\\mbox{}");
282  0 printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{0.9\\linewidth}l}}");
283  0 for (int i = 0; i < list.size(); i++) {
284  0 final String label = (i < ALPHABET.length() ? "" + ALPHABET .charAt(i) : "" + i);
285  0 printer.println("\\centering $" + getLatex(list.getElement(i)) + "$"
286    + " & \\label{" + mainLabel + ":" + label + "} \\hypertarget{" + mainLabel + ":"
287    + label + "}{} \\mbox{\\emph{(" + label + ")}} "
288  0 + (i + 1 < list.size() ? "\\\\" : ""));
289    }
290  0 printer.println("\\end{longtable}");
291    }
292   
293    /**
294    * Print formula.
295    *
296    * @param element Formula to print.
297    */
 
298  0 toggle private void printFormula(final Element element) {
299  0 printer.println("\\mbox{}");
300  0 printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{\\linewidth}}}");
301  0 printer.println("\\centering $" + getLatex(element) + "$");
302  0 printer.println("\\end{longtable}");
303    }
304   
305    /**
306    * Print predicate definition.
307    *
308    * @param definition Print this.
309    * @param title Extra name.
310    * @param id Label for marking this definition.
311    */
 
312  0 toggle private void printPredicateDefinition(final PredicateDefinition definition, final String title,
313    final String id) {
314  0 final StringBuffer define = new StringBuffer("$$" + definition.getLatexPattern());
315  0 final VariableList list = definition.getVariableList();
316  0 if (list != null) {
317  0 for (int i = list.size() - 1; i >= 0; i--) {
318  0 Trace.trace(CLASS, this, "printDefinition", "replacing!");
319  0 StringUtility.replace(define, "#" + (i + 1), getLatex(list.get(i)));
320    }
321    }
322  0 if (definition.getFormula() != null) {
323  0 printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : ""));
324  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
325  0 define.append("\\ :\\leftrightarrow \\ ");
326  0 define.append(getLatex(definition.getFormula().getElement()));
327    } else {
328  0 printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : ""));
329  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
330    }
331  0 define.append("$$");
332  0 elementConverter.addPredicate(definition);
333  0 Trace.param(CLASS, this, "printDefinition", "define", define);
334  0 printer.println(define);
335  0 printer.println(getLatexListEntry(definition.getDescription()));
336  0 if (definition.getFormula() != null) {
337  0 printer.println("\\end{defn}");
338    } else {
339  0 printer.println("\\end{idefn}");
340    }
341    }
342   
343    /**
344    * Print function definition.
345    *
346    * @param definition Print this.
347    * @param title Extra name.
348    * @param id Label for marking this definition.
349    */
 
350  0 toggle private void printFunctionDefinition(final FunctionDefinition definition, final String title,
351    final String id) {
352  0 final StringBuffer define = new StringBuffer("$$" + definition.getLatexPattern());
353  0 final VariableList list = definition.getVariableList();
354  0 if (list != null) {
355  0 for (int i = list.size() - 1; i >= 0; i--) {
356  0 Trace.trace(CLASS, this, "printDefinition", "replacing!");
357  0 StringUtility.replace(define, "#" + (i + 1), getLatex(list.get(i)));
358    }
359    }
360  0 if (definition.getTerm() != null) {
361  0 printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : ""));
362  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
363  0 define.append("\\ := \\ ");
364  0 define.append(getLatex(definition.getTerm().getElement()));
365    } else {
366  0 printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : ""));
367  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
368    }
369  0 define.append("$$");
370  0 elementConverter.addFunction(definition);
371  0 Trace.param(CLASS, this, "printDefinition", "define", define);
372  0 printer.println(define);
373  0 printer.println(getLatexListEntry(definition.getDescription()));
374  0 if (definition.getTerm() != null) {
375  0 printer.println("\\end{defn}");
376    } else {
377  0 printer.println("\\end{idefn}");
378    }
379    }
380   
381    /**
382    * Print proposition.
383    *
384    * @param proposition Print this.
385    * @param title Extra name.
386    * @param id Label for marking this proposition.
387    */
 
388  0 toggle private void printProposition(final Proposition proposition, final String title,
389    final String id) {
390  0 printer.println("\\begin{prop}" + (title != null ? "[" + title + "]" : ""));
391  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
392  0 printTopFormula(proposition.getFormula().getElement(), id);
393  0 printer.println(getLatexListEntry(proposition.getDescription()));
394  0 printer.println("\\end{prop}");
395  0 if (proposition.getProofList() != null) {
396  0 for (int i = 0; i < proposition.getProofList().size(); i++) {
397  0 printer.println("\\begin{proof}");
398  0 printer.println(getLatexListEntry(proposition.getProofList().get(i)
399    .getNonFormalProof()));
400  0 printer.println("\\end{proof}");
401    }
402    }
403    }
404   
405    /**
406    * Print rule declaration.
407    *
408    * @param rule Print this.
409    * @param title Extra name.
410    * @param id Label for marking this proposition.
411    */
 
412  0 toggle private void printRule(final Rule rule, final String title,
413    final String id) {
414  0 printer.println("\\begin{rul}" + (title != null ? "[" + title + "]" : ""));
415  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
416  0 printer.println(getLatexListEntry(rule.getDescription()));
417  0 printer.println("\\end{rul}");
418   
419    // LATER mime 20051210: are these informations equivalent to a formal proof?
420    /*
421    if (null != rule.getLinkList()) {
422    printer.println("\\begin{proof}");
423    printer.println("Rule name: " + rule.getName());
424    printer.println();
425    printer.println();
426    for (int i = 0; i < rule.getLinkList().size(); i++) {
427    printer.println(rule.getLinkList().get(i));
428    }
429    printer.println("\\end{proof}");
430    }
431    */
432  0 if (rule.getProofList() != null) {
433  0 for (int i = 0; i < rule.getProofList().size(); i++) {
434  0 printer.println("\\begin{proof}");
435  0 printer.println(getLatexListEntry(rule.getProofList().get(i)
436    .getNonFormalProof()));
437  0 printer.println("\\end{proof}");
438    }
439    }
440    }
441   
442    /**
443    * Get LaTeX element presentation.
444    *
445    * @param element Print this element.
446    * @return LaTeX form of element.
447    */
 
448  0 toggle private String getLatex(final Element element) {
449  0 return elementConverter.getLatex(element);
450    }
451   
452    /**
453    * Filters correct entry out of LaTeX list. Filter criterion is for example the correct
454    * language.
455    * TODO mime 20050205: filter level too?
456    *
457    * @param list List of LaTeX texts.
458    * @return Filtered text.
459    */
 
460  0 toggle private String getLatexListEntry(final LatexList list) {
461  0 if (list == null) {
462  0 return "";
463    }
464  0 for (int i = 0; i < list.size(); i++) {
465  0 if (language.equals(list.get(i).getLanguage())) {
466  0 return getLatex(list.get(i));
467    }
468    }
469    // assume entry with missing language as default
470  0 for (int i = 0; i < list.size(); i++) {
471  0 if (list.get(i).getLanguage() == null) {
472  0 return getLatex(list.get(i));
473    }
474    }
475  0 for (int i = 0; i < list.size(); i++) { // LATER mime 20050222: evaluate default?
476  0 return "MISSING! OTHER: " + getLatex(list.get(i));
477    }
478  0 return "MISSING!";
479    }
480   
481    /**
482    * Get really LaTeX. Does some simple character replacements for umlauts.
483    * LATER mime 20050205: filter more than German umlauts
484    *
485    * @param latex Unescaped text.
486    * @return Really LaTeX.
487    */
 
488  0 toggle private String getLatex(final Latex latex) {
489  0 if (latex == null || latex.getLatex() == null) {
490  0 return "";
491    }
492  0 return LatexTextParser.transform(latex.getLatex());
493    }
494   
495    }
 
CloverReport generated by Clover Code Coverage v2.3.1
Sa Aug 2 2008 13:56:32 CEST.		   Clover: Open Source License registered to qedeq.org .