Clover Coverage Report
Coverage timestamp: Sa Aug 2 2008 13:56:27 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
../../../../../../img/srcFileCovDistChart9.png 30% of files have more coverage
478   1.018   143   12,58
200   750   0,3   38
38     3,76  
1    
 
  Qedeq2Latex       Line # 79 478 143 84,4% 0.8435754
 
  (3)
 
1    /* $Id: Qedeq2Latex.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.FileInputStream;
22    import java.io.FileOutputStream;
23    import java.io.IOException;
24    import java.io.InputStream;
25   
26    import org.qedeq.base.io.TextOutput;
27    import org.qedeq.base.trace.Trace;
28    import org.qedeq.base.utility.DateUtility;
29    import org.qedeq.base.utility.StringUtility;
30    import org.qedeq.kernel.base.list.Element;
31    import org.qedeq.kernel.base.list.ElementList;
32    import org.qedeq.kernel.base.module.Author;
33    import org.qedeq.kernel.base.module.AuthorList;
34    import org.qedeq.kernel.base.module.Axiom;
35    import org.qedeq.kernel.base.module.Chapter;
36    import org.qedeq.kernel.base.module.FunctionDefinition;
37    import org.qedeq.kernel.base.module.Header;
38    import org.qedeq.kernel.base.module.Import;
39    import org.qedeq.kernel.base.module.ImportList;
40    import org.qedeq.kernel.base.module.Latex;
41    import org.qedeq.kernel.base.module.LatexList;
42    import org.qedeq.kernel.base.module.LinkList;
43    import org.qedeq.kernel.base.module.LiteratureItem;
44    import org.qedeq.kernel.base.module.LiteratureItemList;
45    import org.qedeq.kernel.base.module.LocationList;
46    import org.qedeq.kernel.base.module.Node;
47    import org.qedeq.kernel.base.module.PredicateDefinition;
48    import org.qedeq.kernel.base.module.Proof;
49    import org.qedeq.kernel.base.module.Proposition;
50    import org.qedeq.kernel.base.module.Qedeq;
51    import org.qedeq.kernel.base.module.Rule;
52    import org.qedeq.kernel.base.module.Section;
53    import org.qedeq.kernel.base.module.SectionList;
54    import org.qedeq.kernel.base.module.Specification;
55    import org.qedeq.kernel.base.module.Subsection;
56    import org.qedeq.kernel.base.module.UsedByList;
57    import org.qedeq.kernel.base.module.VariableList;
58    import org.qedeq.kernel.bo.context.KernelContext;
59    import org.qedeq.kernel.bo.module.ControlVisitor;
60    import org.qedeq.kernel.bo.module.KernelQedeqBo;
61    import org.qedeq.kernel.common.DefaultSourceFileExceptionList;
62    import org.qedeq.kernel.common.ModuleAddress;
63    import org.qedeq.kernel.dto.module.NodeVo;
64   
65   
66    /**
67    * Transfer a QEDEQ module into a LaTeX file.
68    * <p>
69    * <b>This is just a quick written generator. No parsing or validation
70    * of inline LaTeX text is done. This class just generates some LaTeX output to be able to
71    * get a visual impression of a QEDEQ module.</b>
72    * <p>
73    * TODO mime 20080330: we should be able to generate a authors help LaTeX document that contains the
74    * labels in the generated document. So referencing is a lot easier...
75    *
76    * @version $Revision: 1.1 $
77    * @author Michael Meyling
78    */
 
79    public final class Qedeq2Latex extends ControlVisitor {
80   
81    /** This class. */
82    private static final Class CLASS = Qedeq2Latex.class;
83   
84    /** Output goes here. */
85    private final TextOutput printer;
86   
87    /** Filter text to get and produce text in this language. */
88    private final String language;
89   
90    /** Filter for this detail level. TODO mime 20080330: not used yet, but we should use it */
91    private final String level;
92   
93    /** Transformer to get LaTeX out of {@link Element}s. */
94    private final Element2Latex elementConverter;
95   
96    /** Current chapter number, starting with 0. */
97    private int chapterNumber;
98   
99    /** Current section number, starting with 0. */
100    private int sectionNumber;
101   
102    /** Current node id. */
103    private String id;
104   
105    /** Current node title. */
106    private String title;
107   
108    /** Alphabet for tagging. */
109    private static final String ALPHABET = "abcdefghijklmnopqrstuvwxyz";
110   
111    /**
112    * Constructor.
113    *
114    * @param prop QEDEQ BO object.
115    * @param printer Print herein.
116    * @param language Filter text to get and produce text in this language only.
117    * @param level Filter for this detail level. LATER mime 20050205: not supported
118    * yet.
119    */
 
120  18 toggle private Qedeq2Latex(final KernelQedeqBo prop,
121    final TextOutput printer,
122    final String language, final String level) {
123  18 super(prop);
124  18 this.printer = printer;
125  18 if (language == null) {
126  0 this.language = "en";
127    } else {
128  18 this.language = language;
129    }
130  18 if (level == null) {
131  0 this.level = "1";
132    } else {
133  18 this.level = level;
134    }
135  18 this.elementConverter = new Element2Latex((prop.hasLoadedRequiredModules()
136    ? prop.getRequiredModules() : null));
137    }
138   
139    /**
140    * Gives a LaTeX representation of given QEDEQ module as InputStream.
141    *
142    * @param prop QEDEQ module.
143    * @param language Filter text to get and produce text in this language only.
144    * @param level Filter for this detail level. LATER mime 20050205: not supported
145    * yet.
146    * @return Resulting LaTeX.
147    * @throws DefaultSourceFileExceptionList Major problem occurred.
148    * @throws IOException
149    */
 
150  18 toggle public static File generateLatex(final KernelQedeqBo prop, final String language,
151    final String level) throws DefaultSourceFileExceptionList, IOException {
152   
153    // first we try to get more information about required modules and their predicates..
154  18 try {
155  18 KernelContext.getInstance().loadRequiredModules(prop.getModuleAddress());
156  18 KernelContext.getInstance().checkModule(prop.getModuleAddress());
157    } catch (Exception e) {
158    // we continue and ignore external predicates
159  0 Trace.trace(CLASS, "print(QedeqBo, TextOutput, String, String)", e);
160  18 };
161  18 String tex = prop.getModuleAddress().getFileName();
162  18 if (tex.toLowerCase().endsWith(".xml")) {
163  18 tex = tex.substring(0, tex.length() - 4);
164    }
165  18 if (language != null && language.length() > 0) {
166  18 tex = tex + "_" + language;
167    }
168    // the destination is the configured destination directory plus the (relative)
169    // localized file (or path) name
170  18 File destination = new File(KernelContext.getInstance().getConfig()
171    .getGenerationDirectory(), tex + ".tex").getCanonicalFile();
172  18 TextOutput printer = null;
173  18 try {
174  18 printer = new TextOutput(prop.getName(), new FileOutputStream(destination));
175  18 final Qedeq2Latex converter = new Qedeq2Latex(prop, printer,
176    language, level);
177  18 converter.traverse();
178    } finally {
179  18 if (printer != null) {
180  18 printer.flush();
181  18 printer.close();
182    }
183    }
184  18 if (printer.checkError()) {
185  0 throw printer.getError();
186    }
187    // FIXME mime 20080520: just for testing purpose the following check is
188    // integrated here after the LaTeX print. The checking results should be maintained
189    // later on as additional information to a module. (Warnings...)
190  18 QedeqBoDuplicateLanguageChecker.check(prop);
191  18 return destination.getCanonicalFile();
192    }
193   
194    /**
195    * Gives a LaTeX representation of given QEDEQ module as InputStream.
196    *
197    * @param prop QEDEQ module.
198    * @param language Filter text to get and produce text in this language only.
199    * @param level Filter for this detail level. LATER mime 20050205: not supported
200    * yet.
201    * @return Resulting LaTeX.
202    * @throws DefaultSourceFileExceptionList Major problem occurred.
203    * @throws IOException
204    */
 
205  18 toggle public static InputStream createLatex(final KernelQedeqBo prop, final String language,
206    final String level) throws IOException, DefaultSourceFileExceptionList {
207  18 return new FileInputStream(generateLatex(prop, language, level));
208    }
209   
 
210  18 toggle public final void visitEnter(final Qedeq qedeq) {
211  18 printer.println("% -*- TeX:" + language.toUpperCase() + " -*-");
212  18 printer.println("%%% ====================================================================");
213  18 printer.println("%%% @LaTeX-file " + printer.getName());
214  18 printer.println("%%% Generated from " + getQedeqBo().getModuleAddress());
215  18 printer.println("%%% Generated at " + DateUtility.getTimestamp());
216  18 printer.println("%%% ====================================================================");
217  18 printer.println();
218  18 printer.println(
219    "%%% Permission is granted to copy, distribute and/or modify this document");
220  18 printer.println("%%% under the terms of the GNU Free Documentation License, Version 1.2");
221  18 printer.println("%%% or any later version published by the Free Software Foundation;");
222  18 printer.println(
223    "%%% with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts.");
224  18 printer.println();
225  18 printer.println("\\documentclass[a4paper,german,10pt,twoside]{book}");
226  18 if ("de".equals(language)) {
227  8 printer.println("\\usepackage[german]{babel}");
228    } else {
229  10 if (!"en".equals(language)) {
230  0 printer.println("%%% TODO unknown language: " + language);
231    }
232  10 printer.println("\\usepackage[english]{babel}");
233    }
234  18 printer.println("\\usepackage{makeidx}");
235  18 printer.println("\\usepackage{amsmath,amsthm,amssymb}");
236  18 printer.println("\\usepackage{color}");
237  18 printer.println("\\usepackage[bookmarks,bookmarksnumbered,bookmarksopen,");
238  18 printer.println(" colorlinks,linkcolor=webgreen,pagebackref]{hyperref}");
239  18 printer.println("\\definecolor{webgreen}{rgb}{0,.5,0}");
240  18 printer.println("\\usepackage{graphicx}");
241  18 printer.println("\\usepackage{xr}");
242  18 printer.println("\\usepackage{epsfig,longtable}");
243  18 printer.println("\\usepackage{tabularx}");
244  18 printer.println();
245  18 if ("de".equals(language)) {
246  8 printer.println("\\newtheorem{thm}{Theorem}[chapter]");
247  8 printer.println("\\newtheorem{cor}[thm]{Korollar}");
248  8 printer.println("\\newtheorem{lem}[thm]{Lemma}");
249  8 printer.println("\\newtheorem{prop}[thm]{Proposition}");
250  8 printer.println("\\newtheorem{ax}{Axiom}");
251  8 printer.println("\\newtheorem{rul}{Regel}");
252  8 printer.println();
253  8 printer.println("\\theoremstyle{definition}");
254  8 printer.println("\\newtheorem{defn}[thm]{Definition}");
255  8 printer.println("\\newtheorem{idefn}[thm]{Initiale Definition}");
256  8 printer.println();
257  8 printer.println("\\theoremstyle{remark}");
258  8 printer.println("\\newtheorem{rem}[thm]{Bemerkung}");
259  8 printer.println("\\newtheorem*{notation}{Notation}");
260    } else {
261  10 if (!"en".equals(language)) {
262  0 printer.println("%%% TODO unknown language: " + language);
263    }
264  10 printer.println("\\newtheorem{thm}{Theorem}[chapter]");
265  10 printer.println("\\newtheorem{cor}[thm]{Corollary}");
266  10 printer.println("\\newtheorem{lem}[thm]{Lemma}");
267  10 printer.println("\\newtheorem{prop}[thm]{Proposition}");
268  10 printer.println("\\newtheorem{ax}{Axiom}");
269  10 printer.println("\\newtheorem{rul}{Rule}");
270  10 printer.println();
271  10 printer.println("\\theoremstyle{definition}");
272  10 printer.println("\\newtheorem{defn}[thm]{Definition}");
273  10 printer.println("\\newtheorem{idefn}[thm]{Initial Definition}");
274  10 printer.println();
275  10 printer.println("\\theoremstyle{remark}");
276  10 printer.println("\\newtheorem{rem}[thm]{Remark}");
277  10 printer.println("\\newtheorem*{notation}{Notation}");
278    }
279  18 printer.println();
280  18 printer.println("\\addtolength{\\textheight}{7\\baselineskip}");
281  18 printer.println("\\addtolength{\\topmargin}{-5\\baselineskip}");
282  18 printer.println();
283  18 printer.println("\\setlength{\\parindent}{0pt}");
284  18 printer.println();
285  18 printer.println("\\frenchspacing \\sloppy");
286  18 printer.println();
287  18 printer.println("\\makeindex");
288  18 printer.println();
289  18 printer.println();
290    }
291   
 
292  18 toggle public final void visitLeave(final Qedeq qedeq) {
293  18 printer.println("\\backmatter");
294  18 printer.println();
295  18 printer.println("\\addcontentsline{toc}{chapter}{\\indexname} \\printindex");
296  18 printer.println();
297  18 printer.println("\\end{document}");
298  18 printer.println();
299    }
300   
 
301  18 toggle public void visitEnter(final Header header) {
302  18 final LatexList tit = header.getTitle();
303  18 printer.print("\\title{");
304  18 printer.print(getLatexListEntry(tit));
305  18 printer.println("}");
306  18 printer.println("\\author{");
307  18 final AuthorList authors = getQedeqBo().getQedeq().getHeader().getAuthorList();
308  36 for (int i = 0; i < authors.size(); i++) {
309  18 if (i > 0) {
310  0 printer.println(", ");
311    }
312  18 final Author author = authors.get(i);
313  18 printer.print(author.getName().getLatex());
314    // TODO mime 20070206 if (author.getEmail() != null)
315    }
316  18 printer.println();
317  18 printer.println("}");
318  18 printer.println();
319  18 printer.println("\\begin{document}");
320  18 printer.println();
321  18 printer.println("\\maketitle");
322  18 printer.println();
323  18 printer.println("\\setlength{\\parskip}{5pt plus 2pt minus 1pt}");
324  18 printer.println("\\mbox{}");
325  18 printer.println("\\vfill");
326  18 printer.println();
327  18 final String url = getQedeqBo().getUrl().toString();
328  18 if (url != null && url.length() > 0) {
329  18 printer.println("\\par");
330  18 if ("de".equals(language)) {
331  8 printer.println("Die Quelle f{\"ur} dieses Dokument ist hier zu finden:");
332    } else {
333  10 if (!"en".equals(language)) {
334  0 printer.println("%%% TODO unknown language: " + language);
335    }
336  10 printer.println("The source for this document can be found here:");
337    }
338  18 printer.println("\\par");
339  18 printer.println("\\url{" + url + "}");
340  18 printer.println();
341    }
342    {
343  18 printer.println("\\par");
344  18 if ("de".equals(language)) {
345  8 printer.println("Die vorliegende Publikation ist urheberrechtlich gesch{\"u}tzt.");
346    } else {
347  10 if (!"en".equals(language)) {
348  0 printer.println("%%% TODO unknown language: " + language);
349    }
350  10 printer.println("Copyright by the authors. All rights reserved.");
351    }
352    }
353  18 final String email = header.getEmail();
354  18 if (email != null && email.length() > 0) {
355  18 final String emailUrl = "\\url{mailto:" + email + "}";
356  18 printer.println("\\par");
357  18 if ("de".equals(language)) {
358  8 printer.println("Bei Fragen, Anregungen oder Bitte um Aufnahme in die Liste der"
359    + " abh{\"a}ngigen Module schicken Sie bitte eine EMail an die Addresse "
360    + emailUrl);
361    } else {
362  10 if (!"en".equals(language)) {
363  0 printer.println("%%% TODO unknown language: " + language);
364    }
365  10 printer.println("If you have any questions, suggestions or want to add something"
366    + " to the list of modules that use this one, please send an email to the"
367    + " address " + emailUrl);
368    }
369  18 printer.println();
370    }
371  18 printer.println("\\setlength{\\parskip}{0pt}");
372  18 printer.println("\\tableofcontents");
373  18 printer.println();
374  18 printer.println("\\setlength{\\parskip}{5pt plus 2pt minus 1pt}");
375  18 printer.println();
376    }
377   
378    /**
379    * Get URL for QEDEQ XML module.
380    *
381    * @param address Current module address.
382    * @param specification Find URL for this location list.
383    * @return URL or <code>""</code> if none (valid?) was found.
384    */
 
385  8 toggle private String getUrl(final ModuleAddress address, final Specification specification) {
386  8 final LocationList list = specification.getLocationList();
387  8 if (list == null || list.size() <= 0) {
388  0 return "";
389    }
390  8 try {
391  8 return address.getModulePaths(specification)[0].getURL().toString();
392    } catch (IOException e) {
393  0 return "";
394    }
395    }
396   
 
397  100 toggle public void visitEnter(final Chapter chapter) {
398  100 printer.print("\\chapter");
399  100 if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) {
400  30 printer.print("*");
401    }
402  100 printer.print("{");
403  100 printer.print(getLatexListEntry(chapter.getTitle()));
404  100 final String label = "chapter" + chapterNumber;
405  100 printer.println("} \\label{" + label + "} \\hypertarget{" + label + "}{}");
406  100 if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) {
407  30 printer.println("\\addcontentsline{toc}{chapter}{"
408    + getLatexListEntry(chapter.getTitle()) + "}");
409    }
410  100 printer.println();
411  100 if (chapter.getIntroduction() != null) {
412  100 printer.println(getLatexListEntry(chapter.getIntroduction()));
413  100 printer.println();
414    }
415    }
416   
 
417  100 toggle public void visitLeave(final Chapter chapter) {
418  100 printer.println("%% end of chapter " + getLatexListEntry(chapter.getTitle()));
419  100 printer.println();
420  100 chapterNumber++; // increase global chapter number
421  100 sectionNumber = 0; // reset section number
422    }
423   
 
424  58 toggle public void visitLeave(final SectionList list) {
425  58 printer.println();
426    }
427   
 
428  172 toggle public void visitEnter(final Section section) {
429    /* LATER mime 20070131: use this information?
430    if (section.getNoNumber() != null) {
431    printer.print(" noNumber=\"" + section.getNoNumber().booleanValue() + "\"");
432    }
433    */
434  172 printer.print("\\section{");
435  172 printer.print(getLatexListEntry(section.getTitle()));
436  172 final String label = "chapter" + chapterNumber + "_section" + sectionNumber;
437  172 printer.println("} \\label{" + label + "} \\hypertarget{" + label + "}{}");
438  172 printer.println(getLatexListEntry(section.getIntroduction()));
439  172 printer.println();
440    }
441   
 
442  172 toggle public void visitLeave(final Section section) {
443  172 sectionNumber++; // increase global section number
444    }
445   
 
446  84 toggle public void visitEnter(final Subsection subsection) {
447    /* LATER mime 20070131: use this information?
448    if (subsection.getId() != null) {
449    printer.print(" id=\"" + subsection.getId() + "\"");
450    }
451    if (subsection.getLevel() != null) {
452    printer.print(" level=\"" + subsection.getLevel() + "\"");
453    }
454    */
455  84 if (subsection.getTitle() != null) {
456  60 printer.print("\\subsection{");
457  60 printer.println(getLatexListEntry(subsection.getTitle()));
458  60 printer.println("}");
459    }
460  84 if (subsection.getId() != null) {
461  0 printer.println("\\label{" + subsection.getId() + "} \\hypertarget{"
462    + subsection.getId() + "}{}");
463    }
464  84 printer.println(getLatexListEntry(subsection.getLatex()));
465    }
466   
 
467  84 toggle public void visitLeave(final Subsection subsection) {
468  84 printer.println();
469  84 printer.println();
470    }
471   
 
472  516 toggle public void visitEnter(final Node node) {
473    /** TODO mime 20070131: level filter
474    if (node.getLevel() != null) {
475    printer.print(" level=\"" + node.getLevel() + "\"");
476    }
477    */
478  516 printer.println("\\par");
479  516 printer.println(getLatexListEntry(node.getPrecedingText()));
480  516 printer.println();
481  516 id = node.getId();
482  516 title = null;
483  516 if (node.getTitle() != null) {
484  288 title = getLatexListEntry(node.getTitle());
485    }
486    }
487   
 
488  516 toggle public void visitLeave(final Node node) {
489  516 printer.println();
490  516 printer.println(getLatexListEntry(node.getSucceedingText()));
491  516 printer.println();
492  516 printer.println();
493    }
494   
 
495  88 toggle public void visitEnter(final Axiom axiom) {
496  88 printer.println("\\begin{ax}" + (title != null ? "[" + title + "]" : ""));
497  88 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
498  88 printFormula(axiom.getFormula().getElement());
499  88 printer.println(getLatexListEntry(axiom.getDescription()));
500  88 printer.println("\\end{ax}");
501    }
502   
 
503  236 toggle public void visitEnter(final Proposition proposition) {
504  236 printer.println("\\begin{prop}" + (title != null ? "[" + title + "]" : ""));
505  236 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
506  236 printTopFormula(proposition.getFormula().getElement(), id);
507  236 printer.println(getLatexListEntry(proposition.getDescription()));
508  236 printer.println("\\end{prop}");
509    }
510   
 
511  40 toggle public void visitEnter(final Proof proof) {
512    /* LATER mime 20070131: filter level and kind
513    if (proof.getKind() != null) {
514    printer.print(" kind=\"" + proof.getKind() + "\"");
515    }
516    if (proof.getLevel() != null) {
517    printer.print(" level=\"" + proof.getLevel() + "\"");
518    }
519    */
520  40 printer.println("\\begin{proof}");
521  40 printer.println(getLatexListEntry(proof.getNonFormalProof()));
522  40 printer.println("\\end{proof}");
523    }
524   
 
525  76 toggle public void visitEnter(final PredicateDefinition definition) {
526  76 final StringBuffer define = new StringBuffer("$$" + definition.getLatexPattern());
527  76 final VariableList list = definition.getVariableList();
528  76 if (list != null) {
529  196 for (int i = list.size() - 1; i >= 0; i--) {
530  128 Trace.trace(CLASS, this, "printPredicateDefinition", "replacing!");
531  128 StringUtility.replace(define, "#" + (i + 1), getLatex(list.get(i)));
532    }
533    }
534  76 if (definition.getFormula() != null) {
535  64 printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : ""));
536  64 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
537  64 define.append("\\ :\\leftrightarrow \\ ");
538  64 define.append(getLatex(definition.getFormula().getElement()));
539    } else {
540  12 printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : ""));
541  12 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
542    }
543  76 define.append("$$");
544    // we always save the definition, even if there already exists an entry
545  76 elementConverter.addPredicate(definition);
546  76 Trace.param(CLASS, this, "printPredicateDefinition", "define", define);
547  76 printer.println(define);
548  76 printer.println(getLatexListEntry(definition.getDescription()));
549  76 if (definition.getFormula() != null) {
550  64 printer.println("\\end{defn}");
551    } else {
552  12 printer.println("\\end{idefn}");
553    }
554    }
555   
 
556  64 toggle public void visitEnter(final FunctionDefinition definition) {
557  64 final StringBuffer define = new StringBuffer("$$" + definition.getLatexPattern());
558  64 final VariableList list = definition.getVariableList();
559  64 if (list != null) {
560  124 for (int i = list.size() - 1; i >= 0; i--) {
561  72 Trace.trace(CLASS, this, "printFunctionDefinition", "replacing!");
562  72 StringUtility.replace(define, "#" + (i + 1), getLatex(list.get(i)));
563    }
564    }
565  64 if (definition.getTerm() != null) {
566  64 printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : ""));
567  64 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
568  64 define.append("\\ := \\ ");
569  64 define.append(getLatex(definition.getTerm().getElement()));
570    } else {
571  0 printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : ""));
572  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
573    }
574  64 define.append("$$");
575    // we always save the definition, even if there already exists an entry
576  64 elementConverter.addFunction(definition);
577  64 Trace.param(CLASS, this, "printFunctionDefinition", "define", define);
578  64 printer.println(define);
579  64 printer.println(getLatexListEntry(definition.getDescription()));
580  64 if (definition.getTerm() != null) {
581  64 printer.println("\\end{defn}");
582    } else {
583  0 printer.println("\\end{idefn}");
584    }
585    }
586   
 
587  64 toggle public void visitLeave(final FunctionDefinition definition) {
588    }
589   
 
590  52 toggle public void visitEnter(final Rule rule) {
591  52 printer.println("\\begin{rul}" + (title != null ? "[" + title + "]" : ""));
592  52 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
593  52 printer.println(getLatexListEntry(rule.getDescription()));
594  52 printer.println("\\end{rul}");
595   
596    // LATER mime 20051210: are these informations equivalent to a formal proof?
597    /*
598    if (null != rule.getLinkList()) {
599    printer.println("\\begin{proof}");
600    printer.println("Rule name: " + rule.getName());
601    printer.println();
602    printer.println();
603    for (int i = 0; i < rule.getLinkList().size(); i++) {
604    printer.println(rule.getLinkList().get(i));
605    }
606    printer.println("\\end{proof}");
607    }
608    */
609  52 if (rule.getProofList() != null) {
610  0 for (int i = 0; i < rule.getProofList().size(); i++) {
611  0 printer.println("\\begin{proof}");
612  0 printer.println(getLatexListEntry(rule.getProofList().get(i)
613    .getNonFormalProof()));
614  0 printer.println("\\end{proof}");
615    }
616    }
617    }
618   
 
619  52 toggle public void visitLeave(final Rule rule) {
620    }
621   
 
622  4 toggle public void visitEnter(final LinkList linkList) {
623  4 if (linkList.size() <= 0) {
624  0 return;
625    }
626  4 if ("de".equals(language)) {
627  2 printer.println("Basierend auf: ");
628    } else {
629  2 if (!"en".equals(language)) {
630  0 printer.println("%%% TODO unknown language: " + language);
631    }
632  2 printer.println("Based on: ");
633    }
634  8 for (int i = 0; i < linkList.size(); i++) {
635  4 if (linkList.get(i) != null) {
636  4 printer.print(" \\ref{" + linkList.get(i) + "}");
637    }
638  4 };
639  4 printer.println();
640    }
641   
 
642  8 toggle public void visitEnter(final LiteratureItemList list) {
643  8 printer.println("\\begin{thebibliography}{99}");
644    // TODO mime 20060926: remove language dependency
645  8 if ("de".equals(language)) {
646  4 printer.println("\\addcontentsline{toc}{chapter}{Literaturverzeichnis}");
647    } else {
648  4 if (!"en".equals(language)) {
649  0 printer.println("%%% TODO unknown language: " + language);
650    }
651  4 printer.println("\\addcontentsline{toc}{chapter}{Bibliography}");
652    }
653  8 final ImportList imports = getQedeqBo().getQedeq().getHeader().getImportList();
654  8 if (imports != null && imports.size() > 0) {
655  4 printer.println();
656  4 printer.println();
657  4 printer.println("%% Used other QEDEQ modules:");
658  8 for (int i = 0; i < imports.size(); i++) {
659  4 final Import imp = imports.get(i);
660  4 printer.print("\\bibitem{" + imp.getLabel() + "} ");
661  4 final Specification spec = imp.getSpecification();
662  4 printer.print(getLatex(spec.getName()));
663  4 if (spec.getLocationList() != null && spec.getLocationList().size() > 0
664    && spec.getLocationList().get(0).getLocation().length() > 0) {
665  4 printer.print(" ");
666    // TODO mime 20070205: later on here must stand the location that was used
667    // to verify the document contents
668    // TODO mime 20070205: convert relative address into absolute
669  4 printer.print("\\url{" + getUrl(getQedeqBo().getModuleAddress(), spec) + "}");
670    }
671  4 printer.println();
672    }
673  4 printer.println();
674  4 printer.println();
675  4 printer.println("%% Other references:");
676  4 printer.println();
677    }
678    }
679   
 
680  8 toggle public void visitLeave(final LiteratureItemList list) {
681  8 final UsedByList usedby = getQedeqBo().getQedeq().getHeader().getUsedByList();
682  8 if (usedby != null && usedby.size() > 0) {
683  4 printer.println();
684  4 printer.println();
685  4 printer.println("%% QEDEQ modules that use this one:");
686  8 for (int i = 0; i < usedby.size(); i++) {
687  4 final Specification spec = usedby.get(i);
688  4 printer.print("\\bibitem{" + spec.getName() + "} ");
689  4 printer.print(getLatex(spec.getName()));
690  4 final String url = getUrl(getQedeqBo().getModuleAddress(), spec);
691  4 if (url != null && url.length() > 0) {
692  4 printer.print(" ");
693  4 printer.print("\\url{" + url + "}");
694    }
695  4 printer.println();
696    }
697  4 printer.println();
698  4 printer.println();
699    }
700  8 printer.println("\\end{thebibliography}");
701    }
702   
 
703  40 toggle public void visitEnter(final LiteratureItem item) {
704  40 printer.print("\\bibitem{" + item.getLabel() + "} ");
705  40 printer.println(getLatexListEntry(item.getItem()));
706  40 printer.println();
707    }
708   
709    /**
710    * Print top level formula. If the formula has the form <code>AND(.., .., ..)</code> the
711    * formula is broken down in several labeled lines.
712    *
713    * @param element Formula to print.
714    * @param mainLabel Main formula label.
715    */
 
716  236 toggle private void printTopFormula(final Element element, final String mainLabel) {
717  236 if (!element.isList() || !element.getList().getOperator().equals("AND")) {
718  164 printFormula(element);
719  164 return;
720    }
721  72 final ElementList list = element.getList();
722  72 printer.println("\\mbox{}");
723  72 printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{0.9\\linewidth}l}}");
724  584 for (int i = 0; i < list.size(); i++) {
725  512 String label = "";
726  512 if (list.size() >= ALPHABET.length() * ALPHABET.length()) {
727  0 label = "" + (i + 1);
728    } else {
729  512 if (list.size() > ALPHABET.length()) {
730  144 final int div = (i / ALPHABET.length());
731  144 label = "" + ALPHABET.charAt(div);
732    }
733  512 label += ALPHABET.charAt(i % ALPHABET.length());
734    }
735    // final String label = (i < ALPHABET.length() ? "" + ALPHABET .charAt(i) : "" + i);
736  512 printer.println("\\centering $" + getLatex(list.getElement(i)) + "$"
737    + " & \\label{" + mainLabel + ":" + label + "} \\hypertarget{" + mainLabel + ":"
738    + label + "}{} \\mbox{\\emph{(" + label + ")}} "
739  512 + (i + 1 < list.size() ? "\\\\" : ""));
740    }
741  72 printer.println("\\end{longtable}");
742    }
743   
744    /**
745    * Print formula.
746    *
747    * @param element Formula to print.
748    */
 
749  252 toggle private void printFormula(final Element element) {
750  252 printer.println("\\mbox{}");
751  252 printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{\\linewidth}}}");
752  252 printer.println("\\centering $" + getLatex(element) + "$");
753  252 printer.println("\\end{longtable}");
754    }
755   
756    /**
757    * Get LaTeX element presentation.
758    *
759    * @param element Print this element.
760    * @return LaTeX form of element.
761    */
 
762  1092 toggle private String getLatex(final Element element) {
763  1092 return elementConverter.getLatex(element);
764    }
765   
766    /**
767    * Filters correct entry out of LaTeX list. Filter criterion is for example the correct
768    * language.
769    * TODO mime 20050205: filter level too?
770    *
771    * @param list List of LaTeX texts.
772    * @return Filtered text.
773    */
 
774  2792 toggle private String getLatexListEntry(final LatexList list) {
775  2792 if (list == null) {
776  952 return "";
777    }
778  2928 for (int i = 0; i < list.size(); i++) {
779  2564 if (language.equals(list.get(i).getLanguage())) {
780  1476 return getLatex(list.get(i));
781    }
782    }
783    // assume entry with missing language as default
784  388 for (int i = 0; i < list.size(); i++) {
785  364 if (list.get(i).getLanguage() == null) {
786  340 return getLatex(list.get(i));
787    }
788    }
789  24 for (int i = 0; i < list.size(); i++) { // LATER mime 20050222: evaluate default?
790  24 return "MISSING! OTHER: " + getLatex(list.get(i));
791    }
792  0 return "MISSING!";
793    }
794   
795    /**
796    * Get really LaTeX. Does some simple character replacements for umlauts. Also transforms
797    * <code>\qref{key}</code> into LaTeX.
798    *
799    * @param latex Unescaped text.
800    * @return Really LaTeX.
801    */
 
802  1840 toggle private String getLatex(final Latex latex) {
803  1840 if (latex == null || latex.getLatex() == null) {
804  10 return "";
805    }
806  1830 StringBuffer result = new StringBuffer(escapeUmlauts(latex.getLatex()));
807   
808    // LATER mime 20080324: check if LaTeX is correct and no forbidden tags are used
809   
810  1830 transformQref(result);
811   
812  1830 return result.toString();
813    }
814   
815    /**
816    * Transform <code>\qref{key}</code> entries into common LaTeX code.
817    *
818    * LATER mime 20080324: write JUnitTests to be sure that no runtime exceptions are thrown if
819    * reference is at end of latex etc.
820    *
821    * @param result Work on this buffer.
822    */
 
823  1830 toggle private void transformQref(final StringBuffer result) {
824  1830 final String method = "transformQref(StringBuffer)";
825  1830 int pos1 = 0;
826  1830 final String qref = "\\qref{";
827  1830 try {
828  ? while (0 <= (pos1 = result.indexOf(qref))) {
829  80 int pos = pos1 + qref.length();
830  80 int pos2 = result.indexOf("}", pos);
831  80 if (pos2 < 0) {
832  0 break;
833    // just let LaTeX find the errors
834    // LATER mime 20080325: add warning
835    }
836  80 String ref = result.substring(pos, pos2);
837  80 Trace.param(CLASS, this, method, "1 ref", ref);
838   
839    // exists a sub reference?
840  80 String sub = "";
841  80 final int posb = pos2 + 1;
842  80 if (posb < result.length() && result.charAt(posb) == '[') {
843  28 pos2 = result.indexOf("]", posb + 1);
844  28 if (pos2 < 0) {
845  0 break;
846    // just let LaTeX find the errors
847    // LATER mime 20080325: add warning
848    }
849  28 sub = result.substring(posb + 1, pos2);
850  28 Trace.param(CLASS, this, method, "sub", sub);
851    }
852   
853    // get module label (if any)
854  80 String label = "";
855  80 int dot = ref.indexOf(".");
856  80 if (dot >= 0) {
857  24 label = ref.substring(0, dot);
858  24 ref = ref.substring(dot + 1);
859    }
860  80 if (label.length() == 0) {
861  56 if (getQedeqBo().getKernelRequiredModules().getQedeqBo(ref) != null) {
862  4 label = ref;
863  4 ref = "";
864    }
865    }
866  80 Trace.param(CLASS, this, method, "2 ref", ref);
867  80 Trace.param(CLASS, this, method, "2 label", label);
868  80 KernelQedeqBo prop = getQedeqBo();
869  80 if (label.length() > 0) {
870  28 prop = prop.getKernelRequiredModules().getKernelQedeqBo(label);
871    }
872  80 NodeVo node = null;
873  80 if (prop != null) {
874  80 if (prop.getLabels() != null) {
875  80 node = prop.getLabels().getNode(ref);
876    } else {
877  0 Trace.info(CLASS, this, method, "no labels found");
878    }
879    }
880  80 if (node == null) {
881  4 Trace.info(CLASS, this, method, "node not found for " + ref);
882    }
883  80 if (label.length() <= 0) {
884  52 final String display = getDisplay(ref, node);
885  52 result.replace(pos1, pos2 + 1, display + "~\\ref{" + ref + "}"
886  52 + (sub.length() > 0 ? " (" + sub + ")" : ""));
887    } else {
888  28 if (ref.length() <= 0) {
889  4 result.replace(pos1, pos2 + 1, "\\url{" + getPdfLink(prop) + "}");
890    } else {
891  24 final String display = getDisplay(ref, node);
892  24 result.replace(pos1, pos2 + 1, "\\hyperref{" + getPdfLink(prop) + "}{}{"
893  24 + ref + (sub.length() > 0 ? ":" + sub : "")
894  24 + "}{" + display + (sub.length() > 0 ? " (" + sub + ")" : "") + "}");
895    }
896    }
897    }
898    } catch (RuntimeException e) {
899  0 Trace.trace(CLASS, this, method, e);
900    }
901    }
902   
903    /**
904    * Get text to display for a link.
905    * TODO mime 20080330: refactor language dependent code
906    *
907    * @param ref Reference label.
908    * @param node Node to link to. Might be <code>null</code>.
909    * @return Display text.
910    */
 
911  76 toggle private String getDisplay(final String ref, final NodeVo node) {
912  76 String display = ref;
913  76 if (node != null) {
914  76 if (node.getName() != null) {
915  40 display = getLatexListEntry(node.getName());
916    } else {
917  36 if (node.getNodeType() instanceof Axiom) {
918  0 if ("de".equals(language)) {
919  0 display = "Axiom";
920    } else {
921  0 display = "axiom";
922    }
923  36 } else if (node.getNodeType() instanceof Proposition) {
924  36 if ("de".equals(language)) {
925  16 display = "Proposition";
926    } else {
927  20 display = "proposition";
928    }
929  0 } else if (node.getNodeType() instanceof FunctionDefinition) {
930  0 if ("de".equals(language)) {
931  0 display = "Definition";
932    } else {
933  0 display = "definition";
934    }
935  0 } else if (node.getNodeType() instanceof PredicateDefinition) {
936  0 if ("de".equals(language)) {
937  0 display = "Definition";
938    } else {
939  0 display = "definition";
940    }
941  0 } else if (node.getNodeType() instanceof Rule) {
942  0 if ("de".equals(language)) {
943  0 display = "Regel";
944    } else {
945  0 display = "rule";
946    }
947    } else {
948  0 if ("de".equals(language)) {
949  0 display = "Unbekannt";
950    } else {
951  0 display = "unknown";
952    }
953    }
954    }
955    }
956  76 return display;
957    }
958   
959    /**
960    * Get URL to for PDF version of module.
961    *
962    * @param prop Get URL for this QEDEQ module.
963    * @return URL to PDF.
964    */
 
965  28 toggle private String getPdfLink(final KernelQedeqBo prop) {
966  28 final String url = prop.getUrl().toString();
967  28 final int dot = url.lastIndexOf(".");
968  28 return url.substring(0, dot) + "_" + language + ".pdf";
969    }
970   
971    /**
972    * Get LaTeX from string. Escapes common characters.
973    *
974    * @param text Unescaped text.
975    * @return LaTeX.
976    */
 
977  8 toggle private String getLatex(final String text) {
978  8 final StringBuffer buffer = new StringBuffer(text);
979  8 StringUtility.deleteLineLeadingWhitespace(buffer);
980  8 StringUtility.replace(buffer, "\\", "\\textbackslash");
981  8 StringUtility.replace(buffer, "$", "\\$");
982  8 StringUtility.replace(buffer, "&", "\\&");
983  8 StringUtility.replace(buffer, "%", "\\%");
984  8 StringUtility.replace(buffer, "#", "\\#");
985  8 StringUtility.replace(buffer, "_", "\\_");
986  8 StringUtility.replace(buffer, "{", "\\{");
987  8 StringUtility.replace(buffer, "}", "\\}");
988  8 StringUtility.replace(buffer, "~", "\\textasciitilde");
989  8 StringUtility.replace(buffer, "^", "\\textasciicircum");
990  8 StringUtility.replace(buffer, "<", "\\textless");
991  8 StringUtility.replace(buffer, ">", "\\textgreater");
992  8 return escapeUmlauts(buffer.toString());
993    }
994   
995    /**
996    * Get really LaTeX. Does some simple character replacements for umlauts.
997    * LATER mime 20050205: filter more than German umlauts
998    *
999    * @param nearlyLatex Unescaped text.
1000    * @return Really LaTeX.
1001    */
 
1002  1838 toggle private String escapeUmlauts(final String nearlyLatex) {
1003  1838 if (nearlyLatex == null) {
1004  0 return "";
1005    }
1006  1838 final StringBuffer buffer = new StringBuffer(nearlyLatex);
1007  1838 StringUtility.deleteLineLeadingWhitespace(buffer);
1008  1838 StringUtility.replace(buffer, "\u00fc", "{\\\"u}");
1009  1838 StringUtility.replace(buffer, "\u00f6", "{\\\"o}");
1010  1838 StringUtility.replace(buffer, "\u00e4", "{\\\"a}");
1011  1838 StringUtility.replace(buffer, "\u00dc", "{\\\"U}");
1012  1838 StringUtility.replace(buffer, "\u00d6", "{\\\"O}");
1013  1838 StringUtility.replace(buffer, "\u00c4", "{\\\"A}");
1014  1838 StringUtility.replace(buffer, "\u00df", "{\\ss}");
1015  1838 return buffer.toString();
1016    }
1017   
1018    }
 
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 .