Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
Overview   Package   File
    FRAMES   NO FRAMES     
../../../../../../img/srcFileCovDistChart8.png 62% of files have more coverage
789   1,677   309   9.86
384   1,327   0.39   80
80     3.86  
1    
 
  Qedeq2LatexExecutor       Line # 105 789 309 80.2% 0.802075
 
  (10)
 
1    /* This file is part of the project "Hilbert II" - http://www.qedeq.org
2    *
3    * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
4    *
5    * "Hilbert II" is free software; you can redistribute
6    * it and/or modify it under the terms of the GNU General Public
7    * License as published by the Free Software Foundation; either
8    * version 2 of the License, or (at your option) any later version.
9    *
10    * This program is distributed in the hope that it will be useful,
11    * but WITHOUT ANY WARRANTY; without even the implied warranty of
12    * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13    * GNU General Public License for more details.
14    */
15   
16    package org.qedeq.kernel.bo.service.latex;
17   
18    import java.io.File;
19    import java.io.FileInputStream;
20    import java.io.FileOutputStream;
21    import java.io.IOException;
22    import java.io.InputStream;
23    import java.util.Locale;
24   
25    import org.qedeq.base.io.IoUtility;
26    import org.qedeq.base.io.Parameters;
27    import org.qedeq.base.io.SourcePosition;
28    import org.qedeq.base.io.TextInput;
29    import org.qedeq.base.io.TextOutput;
30    import org.qedeq.base.trace.Trace;
31    import org.qedeq.base.utility.DateUtility;
32    import org.qedeq.base.utility.EqualsUtility;
33    import org.qedeq.base.utility.StringUtility;
34    import org.qedeq.kernel.bo.log.QedeqLog;
35    import org.qedeq.kernel.bo.module.ControlVisitor;
36    import org.qedeq.kernel.bo.module.InternalServiceCall;
37    import org.qedeq.kernel.bo.module.KernelNodeBo;
38    import org.qedeq.kernel.bo.module.KernelQedeqBo;
39    import org.qedeq.kernel.bo.module.PluginExecutor;
40    import org.qedeq.kernel.bo.module.Reference;
41    import org.qedeq.kernel.se.base.list.Element;
42    import org.qedeq.kernel.se.base.list.ElementList;
43    import org.qedeq.kernel.se.base.module.Add;
44    import org.qedeq.kernel.se.base.module.Author;
45    import org.qedeq.kernel.se.base.module.AuthorList;
46    import org.qedeq.kernel.se.base.module.Axiom;
47    import org.qedeq.kernel.se.base.module.ChangedRule;
48    import org.qedeq.kernel.se.base.module.ChangedRuleList;
49    import org.qedeq.kernel.se.base.module.Chapter;
50    import org.qedeq.kernel.se.base.module.Conclusion;
51    import org.qedeq.kernel.se.base.module.ConditionalProof;
52    import org.qedeq.kernel.se.base.module.Existential;
53    import org.qedeq.kernel.se.base.module.FormalProof;
54    import org.qedeq.kernel.se.base.module.FormalProofLine;
55    import org.qedeq.kernel.se.base.module.FormalProofLineList;
56    import org.qedeq.kernel.se.base.module.FunctionDefinition;
57    import org.qedeq.kernel.se.base.module.Header;
58    import org.qedeq.kernel.se.base.module.Hypothesis;
59    import org.qedeq.kernel.se.base.module.Import;
60    import org.qedeq.kernel.se.base.module.ImportList;
61    import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
62    import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
63    import org.qedeq.kernel.se.base.module.Latex;
64    import org.qedeq.kernel.se.base.module.LatexList;
65    import org.qedeq.kernel.se.base.module.LinkList;
66    import org.qedeq.kernel.se.base.module.LiteratureItem;
67    import org.qedeq.kernel.se.base.module.LiteratureItemList;
68    import org.qedeq.kernel.se.base.module.LocationList;
69    import org.qedeq.kernel.se.base.module.ModusPonens;
70    import org.qedeq.kernel.se.base.module.Node;
71    import org.qedeq.kernel.se.base.module.PredicateDefinition;
72    import org.qedeq.kernel.se.base.module.Proof;
73    import org.qedeq.kernel.se.base.module.Proposition;
74    import org.qedeq.kernel.se.base.module.Qedeq;
75    import org.qedeq.kernel.se.base.module.Rename;
76    import org.qedeq.kernel.se.base.module.Rule;
77    import org.qedeq.kernel.se.base.module.Section;
78    import org.qedeq.kernel.se.base.module.SectionList;
79    import org.qedeq.kernel.se.base.module.Specification;
80    import org.qedeq.kernel.se.base.module.Subsection;
81    import org.qedeq.kernel.se.base.module.SubsectionList;
82    import org.qedeq.kernel.se.base.module.SubsectionType;
83    import org.qedeq.kernel.se.base.module.SubstFree;
84    import org.qedeq.kernel.se.base.module.SubstFunc;
85    import org.qedeq.kernel.se.base.module.SubstPred;
86    import org.qedeq.kernel.se.base.module.Universal;
87    import org.qedeq.kernel.se.base.module.UsedByList;
88    import org.qedeq.kernel.se.common.ModuleAddress;
89    import org.qedeq.kernel.se.common.ModuleContext;
90    import org.qedeq.kernel.se.common.ModuleDataException;
91    import org.qedeq.kernel.se.common.Plugin;
92    import org.qedeq.kernel.se.common.RuleKey;
93    import org.qedeq.kernel.se.common.SourceFileExceptionList;
94   
95   
96    /**
97    * Transfer a QEDEQ module into a LaTeX file.
98    * <p>
99    * <b>This is just a quick written generator. No parsing or validation
100    * of inline LaTeX text is done. This class just generates some LaTeX output to be able to
101    * get a visual impression of a QEDEQ module.</b>
102    *
103    * @author Michael Meyling
104    */
 
105    public final class Qedeq2LatexExecutor extends ControlVisitor implements PluginExecutor {
106   
107    /** This class. */
108    private static final Class CLASS = Qedeq2LatexExecutor.class;
109   
110    // TODO m31 20100316: check number area for error codes
111    // TODO m31 20100803: add JUnit tests for all error codes
112   
113    /** Output goes here. */
114    private TextOutput printer;
115   
116    /** Filter text to get and produce text in this language. */
117    private String language;
118   
119    /** Filter for this detail level. */
120    // private String level;
121   
122    /** Should additional information be put into LaTeX output? E.g. QEDEQ reference names. */
123    private final boolean info;
124   
125    /** Should only names and formulas be be printed? */
126    private final boolean brief;
127   
128    /** Current node id. */
129    private String id;
130   
131    /** Current node title. */
132    private String title;
133   
134    /** Sub context like "getIntroduction()". */
135    private String subContext = "";
136   
137    /** Remembered proof line label. */
138    private String label = "";
139   
140    /** Remembered proof line formula. */
141    private String formula = "";
142   
143    /** Remembered proof line reason. */
144    private String reason = "";
145   
146    /** Remembered proof line tabulator level. */
147    private int tabLevel = 0;
148   
149    /** Alphabet for tagging. */
150    private static final String ALPHABET = "abcdefghijklmnopqrstuvwxyz";
151   
152    /**
153    * Constructor.
154    *
155    * @param plugin This plugin we work for.
156    * @param prop QEDEQ BO object.
157    * @param parameters Parameters.
158    */
 
159  42 toggle public Qedeq2LatexExecutor(final Plugin plugin, final KernelQedeqBo prop, final Parameters parameters) {
160  42 super(plugin, prop);
161  42 info = parameters.getBoolean("info");
162  42 brief = parameters.getBoolean("brief");
163    }
164   
 
165  46 toggle private Plugin getPlugin() {
166  46 return (Plugin) getService();
167    }
168   
 
169  4 toggle public Object executePlugin(final InternalServiceCall call, final Object data) {
170  4 final String method = "executePlugin(QedeqBo, Map)";
171  4 try {
172  4 QedeqLog.getInstance().logRequest("Generate LaTeX", getQedeqBo().getUrl());
173  4 final String[] languages = getQedeqBo().getSupportedLanguages();
174  12 for (int j = 0; j < languages.length; j++) {
175  8 language = languages[j];
176    // level = "1";
177  8 final String result = generateLatex(call, languages[j], "1").toString();
178  8 if (languages[j] != null) {
179  8 QedeqLog.getInstance().logSuccessfulReply(
180    "LaTeX for language \"" + languages[j]
181    + "\" was generated from into \"" + result + "\"", getQedeqBo().getUrl());
182    } else {
183  0 QedeqLog.getInstance().logSuccessfulReply(
184    "LaTeX for default language "
185    + "was generated into \"" + result + "\"", getQedeqBo().getUrl());
186    }
187    }
188  4 if (languages.length == 0) {
189  0 QedeqLog.getInstance().logMessage("no supported language found, assuming 'en'");
190  0 final String result = generateLatex(call, "en", "1").toString();
191  0 QedeqLog.getInstance().logSuccessfulReply(
192    "LaTeX for language \"en"
193    + "\" was generated into \"" + result + "\"", getQedeqBo().getUrl());
194    }
195    } catch (final SourceFileExceptionList e) {
196  0 final String msg = "Generation failed";
197  0 Trace.fatal(CLASS, this, method, msg, e);
198  0 QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(), e.getMessage());
199    } catch (IOException e) {
200  0 final String msg = "Generation failed";
201  0 Trace.fatal(CLASS, this, method, msg, e);
202  0 QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(), e.getMessage());
203    } catch (final RuntimeException e) {
204  0 Trace.fatal(CLASS, this, method, "unexpected problem", e);
205  0 QedeqLog.getInstance().logFailureReply(
206    "Generation failed", getQedeqBo().getUrl(), "unexpected problem: "
207  0 + (e.getMessage() != null ? e.getMessage() : e.toString()));
208    }
209  4 return null;
210    }
211   
212    /**
213    * Get an input stream for the LaTeX creation.
214    *
215    * @param call This process executes us.
216    * @param language Filter text to get and produce text in this language only.
217    * @param level Filter for this detail level. LATER mime 20050205: not supported
218    * yet.
219    * @return Resulting LaTeX.
220    * @throws SourceFileExceptionList Major problem occurred.
221    * @throws IOException File IO failed.
222    */
 
223  38 toggle public InputStream createLatex(final InternalServiceCall call, final String language, final String level)
224    throws SourceFileExceptionList, IOException {
225  38 return new FileInputStream(generateLatex(call, language, level));
226    }
227   
228    /**
229    * Gives a LaTeX representation of given QEDEQ module as InputStream.
230    *
231    * @param call This process executes us.
232    * @param language Filter text to get and produce text in this language only.
233    * <code>null</code> is ok.
234    * @param level Filter for this detail level. LATER mime 20050205: not supported
235    * yet.
236    * @return Resulting LaTeX.
237    * @throws SourceFileExceptionList Major problem occurred.
238    * @throws IOException File IO failed.
239    */
 
240  46 toggle public File generateLatex(final InternalServiceCall call, final String language, final String level)
241    throws SourceFileExceptionList, IOException {
242  46 final String method = "generateLatex(String, String)";
243  46 this.language = language;
244    // this.level = level;
245    // first we try to get more information about required modules and their predicates..
246  46 try {
247  46 getServices().loadRequiredModules(call.getInternalServiceProcess(), getQedeqBo());
248  46 getServices().checkWellFormedness(call.getInternalServiceProcess(), getQedeqBo());
249    } catch (Exception e) {
250    // we continue and ignore external predicates
251  0 Trace.trace(CLASS, method, e);
252    }
253  46 String tex = getQedeqBo().getModuleAddress().getFileName();
254  46 if (tex.toLowerCase(Locale.US).endsWith(".xml")) {
255  46 tex = tex.substring(0, tex.length() - 4);
256    }
257  46 if (language != null && language.length() > 0) {
258  46 tex = tex + "_" + language;
259    }
260    // the destination is the configured destination directory plus the (relative)
261    // localized file (or path) name
262  46 File destination = new File(getServices().getConfig()
263    .getGenerationDirectory(), tex + ".tex").getCanonicalFile();
264   
265  46 init();
266   
267  46 try {
268    // TODO 20110204 m31: here we should choose the correct encoding; perhaps GUI configurable?
269  46 if ("de".equals(language)) {
270  18 printer = new TextOutput(getQedeqBo().getName(), new FileOutputStream(destination),
271    "ISO-8859-1") {
 
272  227172 toggle public void append(final String txt) {
273  227172 super.append(escapeUmlauts(txt));
274    }
275    };
276    } else {
277  28 printer = new TextOutput(getQedeqBo().getName(), new FileOutputStream(destination),
278    "UTF-8") {
 
279  306048 toggle public void append(final String txt) {
280  306048 super.append(escapeUmlauts(txt));
281    }
282    };
283    }
284  46 traverse(call.getInternalServiceProcess());
285    } finally {
286  46 getQedeqBo().addPluginErrorsAndWarnings(getPlugin(), getErrorList(), getWarningList());
287  46 if (printer != null) {
288  46 printer.flush();
289  46 printer.close();
290    }
291    }
292  46 if (printer != null && printer.checkError()) {
293  0 throw printer.getError();
294    }
295  46 try {
296  46 QedeqBoDuplicateLanguageChecker.check(call);
297    } catch (SourceFileExceptionList warnings) {
298  0 getQedeqBo().addPluginErrorsAndWarnings(getPlugin(), null, warnings);
299    }
300  46 return destination.getCanonicalFile();
301    }
302   
303    /**
304    * Reset counters and other variables. Should be executed before {@link #traverse()}.
305    */
 
306  46 toggle protected void init() {
307  46 id = null;
308  46 title = null;
309  46 subContext = "";
310    }
311   
 
312  46 toggle public final void visitEnter(final Qedeq qedeq) {
313  46 printer.println("% -*- TeX"
314  46 + (language != null ? ":" + language.toUpperCase(Locale.US) : "") + " -*-");
315  46 printer.println("%%% ====================================================================");
316  46 printer.println("%%% @LaTeX-file " + printer.getName());
317  46 printer.println("%%% Generated from " + getQedeqBo().getModuleAddress());
318  46 printer.println("%%% Generated at " + DateUtility.getTimestamp());
319  46 printer.println("%%% ====================================================================");
320  46 printer.println();
321  46 printer.println(
322    "%%% Permission is granted to copy, distribute and/or modify this document");
323  46 printer.println("%%% under the terms of the GNU Free Documentation License, Version 1.2");
324  46 printer.println("%%% or any later version published by the Free Software Foundation;");
325  46 printer.println(
326    "%%% with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts.");
327  46 printer.println();
328  46 printer.println("\\documentclass[a4paper,german,10pt,twoside]{book}");
329  46 if ("de".equals(language)) {
330  18 printer.println("\\usepackage[german]{babel}");
331    } else {
332  28 if (!"en".equals(language)) {
333  0 printer.println("%%% TODO unknown language: " + language);
334    }
335  28 printer.println("\\usepackage[english]{babel}");
336    }
337  46 printer.println("\\usepackage{makeidx}");
338  46 printer.println("\\usepackage{amsmath,amsthm,amssymb}");
339  46 printer.println("\\usepackage{color}");
340  46 printer.println("\\usepackage{xr}");
341  46 printer.println("\\usepackage{tabularx}");
342    // printer.println("\\usepackage{epsfig,longtable}");
343    // printer.println("\\usepackage{ltabptch}"); // not installed on our server
344  46 printer.println("\\usepackage[bookmarks=true,bookmarksnumbered,bookmarksopen,");
345  46 printer.println(" unicode=true,colorlinks=true,linkcolor=webgreen,");
346  46 printer.println(" pagebackref=true,pdfnewwindow=true,pdfstartview=FitH]{hyperref}");
347  46 printer.println("\\definecolor{webgreen}{rgb}{0,.5,0}");
348  46 printer.println("\\usepackage{epsfig,longtable}");
349  46 printer.println("\\usepackage{graphicx}");
350  46 printer.println("\\usepackage[all]{hypcap}");
351  46 printer.println();
352  46 if ("de".equals(language)) {
353    // TODO m31 20100313: validate different counter types
354    // printer.println("\\newtheorem{thm}{Theorem}[chapter]");
355  18 printer.println("\\newtheorem{thm}{Theorem}");
356  18 printer.println("\\newtheorem{cor}[thm]{Korollar}");
357  18 printer.println("\\newtheorem{lem}[thm]{Lemma}");
358  18 printer.println("\\newtheorem{prop}[thm]{Proposition}");
359  18 printer.println("\\newtheorem{ax}{Axiom}");
360  18 printer.println("\\newtheorem{rul}{Regel}");
361  18 printer.println();
362  18 printer.println("\\theoremstyle{definition}");
363  18 printer.println("\\newtheorem{defn}{Definition}");
364  18 printer.println("\\newtheorem{idefn}[defn]{Initiale Definition}");
365  18 printer.println();
366  18 printer.println("\\theoremstyle{remark}");
367  18 printer.println("\\newtheorem{rem}[thm]{Bemerkung}");
368  18 printer.println("\\newtheorem*{notation}{Notation}");
369    } else {
370  28 if (!"en".equals(language)) {
371  0 printer.println("%%% TODO unknown language: " + language);
372    }
373    // TODO m31 20100313: validate different counter types
374    // printer.println("\\newtheorem{thm}{Theorem}[chapter]");
375  28 printer.println("\\newtheorem{thm}{Theorem}");
376  28 printer.println("\\newtheorem{cor}[thm]{Corollary}");
377  28 printer.println("\\newtheorem{lem}[thm]{Lemma}");
378  28 printer.println("\\newtheorem{prop}[thm]{Proposition}");
379  28 printer.println("\\newtheorem{ax}{Axiom}");
380  28 printer.println("\\newtheorem{rul}{Rule}");
381  28 printer.println();
382  28 printer.println("\\theoremstyle{definition}");
383  28 printer.println("\\newtheorem{defn}{Definition}");
384  28 printer.println("\\newtheorem{idefn}[defn]{Initial Definition}");
385  28 printer.println();
386  28 printer.println("\\theoremstyle{remark}");
387  28 printer.println("\\newtheorem{rem}[thm]{Remark}");
388  28 printer.println("\\newtheorem*{notation}{Notation}");
389    }
390  46 printer.println();
391  46 printer.println();
392  46 printer.println("\\addtolength{\\textheight}{7\\baselineskip}");
393  46 printer.println("\\addtolength{\\topmargin}{-5\\baselineskip}");
394  46 printer.println();
395  46 printer.println("\\setlength{\\parindent}{0pt}");
396  46 printer.println();
397  46 printer.println("\\frenchspacing \\sloppy");
398  46 printer.println();
399  46 printer.println("\\makeindex");
400  46 printer.println();
401  46 printer.println();
402    }
403   
 
404  46 toggle public final void visitLeave(final Qedeq qedeq) {
405  46 printer.println("\\addcontentsline{toc}{chapter}{\\indexname} \\printindex");
406  46 printer.println();
407  46 printer.println("\\end{document}");
408  46 printer.println();
409    }
410   
 
411  46 toggle public void visitEnter(final Header header) {
412  46 final LatexList tit = header.getTitle();
413  46 printer.print("\\title{");
414  46 printer.print(getLatexListEntry("getTitle()", tit));
415  46 printer.println("}");
416  46 printer.println("\\author{");
417  46 final AuthorList authors = getQedeqBo().getQedeq().getHeader().getAuthorList();
418  46 final StringBuffer authorList = new StringBuffer();
419  92 for (int i = 0; i < authors.size(); i++) {
420  46 if (i > 0) {
421  0 authorList.append(", ");
422  0 printer.println(", ");
423    }
424  46 final Author author = authors.get(i);
425  46 final String name = author.getName().getLatex().trim();
426  46 printer.print(name);
427  46 authorList.append(name);
428  46 String email = author.getEmail();
429  46 if (email != null && email.trim().length() > 0) {
430  46 authorList.append(" \\href{mailto:" + email + "}{" + email + "}");
431    }
432    }
433  46 printer.println();
434  46 printer.println("}");
435  46 printer.println();
436  46 printer.println("\\begin{document}");
437  46 printer.println();
438  46 printer.println("\\maketitle");
439  46 printer.println();
440  46 printer.println("\\setlength{\\parskip}{5pt plus 2pt minus 1pt}");
441  46 printer.println("\\mbox{}");
442  46 printer.println("\\vfill");
443  46 printer.println();
444  46 final String url = getQedeqBo().getUrl();
445  46 if (url != null && url.length() > 0) {
446  46 printer.println("\\par");
447  46 if ("de".equals(language)) {
448  18 printer.println("Die Quelle f{\"ur} dieses Dokument ist hier zu finden:");
449    } else {
450  28 if (!"en".equals(language)) {
451  0 printer.println("%%% TODO unknown language: " + language);
452    }
453  28 printer.println("The source for this document can be found here:");
454    }
455  46 printer.println("\\par");
456  46 printer.println("\\url{" + url + "}");
457  46 printer.println();
458    }
459    {
460  46 printer.println("\\par");
461  46 if ("de".equals(language)) {
462  18 printer.println("Die vorliegende Publikation ist urheberrechtlich gesch{\"u}tzt.");
463    } else {
464  28 if (!"en".equals(language)) {
465  0 printer.println("%%% TODO unknown language: " + language);
466    }
467  28 printer.println("Copyright by the authors. All rights reserved.");
468    }
469    }
470  46 final String email = header.getEmail();
471  46 if (email != null && email.length() > 0) {
472  46 final String emailUrl = "\\href{mailto:" + email + "}{" + email + "}";
473  46 printer.println("\\par");
474  46 if ("de".equals(language)) {
475  18 printer.println("Bei Fragen, Anregungen oder Bitte um Aufnahme in die Liste der"
476    + " abh\u00e4ngigen Module schicken Sie bitte eine EMail an die Adresse "
477    + emailUrl);
478  18 printer.println();
479  18 printer.println("\\par");
480  18 printer.println("Die Autoren dieses Dokuments sind:");
481  18 printer.println(authorList);
482    } else {
483  28 if (!"en".equals(language)) {
484  0 printer.println("%%% TODO unknown language: " + language);
485    }
486  28 printer.println("If you have any questions, suggestions or want to add something"
487    + " to the list of modules that use this one, please send an email to the"
488    + " address " + emailUrl);
489  28 printer.println();
490  28 printer.println("\\par");
491  28 printer.println("The authors of this document are:");
492  28 printer.println(authorList);
493    }
494  46 printer.println();
495    }
496    }
497   
 
498  46 toggle public void visitLeave(final Header header) {
499  46 printer.println();
500  46 printer.println();
501  46 printer.println("\\setlength{\\parskip}{0pt}");
502  46 printer.println("\\tableofcontents");
503  46 printer.println();
504  46 printer.println("\\setlength{\\parskip}{5pt plus 2pt minus 1pt}");
505  46 printer.println();
506    }
507   
 
508  22 toggle public void visitEnter(final ImportList imports) throws ModuleDataException {
509  22 printer.println();
510  22 printer.println();
511  22 printer.println("\\par");
512  22 if ("de".equals(language)) {
513  10 printer.println("Benutzte QEDEQ module:");
514    } else {
515  12 if (!"en".equals(language)) {
516  0 printer.println("%%% TODO unknown language: " + language);
517    }
518  12 printer.println("Used other QEDEQ modules:");
519    }
520  22 printer.println();
521  22 printer.println("\\par");
522  22 printer.println();
523    }
524   
 
525  32 toggle public void visitEnter(final Import imp) throws ModuleDataException {
526  32 printer.println();
527  32 printer.println("\\par");
528  32 printer.print("\\textbf{" + imp.getLabel() + "} ");
529  32 final Specification spec = imp.getSpecification();
530  32 printer.print(getLatex(spec.getName()));
531  32 if (spec.getLocationList() != null && spec.getLocationList().size() > 0
532    && spec.getLocationList().get(0).getLocation().length() > 0) {
533  32 printer.print(" ");
534  32 printer.print("\\url{" + getPdfLink((KernelQedeqBo) getQedeqBo()
535    .getLabels().getReferences().getQedeqBo(imp.getLabel())) + "}");
536    }
537  32 printer.println();
538    }
539   
540    /**
541    * Get URL for QEDEQ XML module.
542    *
543    * @param address Current module address.
544    * @param specification Find URL for this location list.
545    * @return URL or <code>""</code> if none (valid?) was found.
546    */
 
547  8 toggle private String getUrl(final ModuleAddress address, final Specification specification) {
548  8 final LocationList list = specification.getLocationList();
549  8 if (list == null || list.size() <= 0) {
550  0 return "";
551    }
552  8 try {
553  8 return address.getModulePaths(specification)[0].getUrl();
554    } catch (IOException e) {
555  0 return "";
556    }
557    }
558   
 
559  146 toggle public void visitEnter(final Chapter chapter) {
560    // check if we print only brief and test for non text subnodes
561  146 if (brief) {
562  0 boolean hasFormalContent = false;
563  0 do {
564  0 final SectionList sections = chapter.getSectionList();
565  0 if (sections == null) {
566  0 break;
567    }
568  0 for (int i = 0; i < sections.size() && !hasFormalContent; i++) {
569  0 final Section section = sections.get(i);
570  0 if (section == null) {
571  0 continue;
572    }
573  0 final SubsectionList subSections = section.getSubsectionList();
574  0 if (subSections == null) {
575  0 continue;
576    }
577  0 for (int j = 0; j < subSections.size(); j++) {
578  0 final SubsectionType subSection = subSections.get(j);
579  0 if (!(subSection instanceof Subsection)) {
580  0 hasFormalContent = true;
581  0 break;
582    }
583    }
584    }
585    } while (false);
586  0 if (!hasFormalContent) {
587  0 setBlocked(true);
588  0 return;
589    }
590    }
591  146 printer.print("\\chapter");
592  146 if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) {
593  34 printer.print("*");
594    }
595  146 printer.print("{");
596  146 printer.print(getLatexListEntry("getTitle()", chapter.getTitle()));
597  146 final String chapterLabel = "chapter" + getCurrentNumbers().getAbsoluteChapterNumber();
598  146 printer.println("} \\label{" + chapterLabel + "} \\hypertarget{" + chapterLabel + "}{}");
599  146 if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) {
600  34 printer.println("\\addcontentsline{toc}{chapter}{"
601    + getLatexListEntry("getTitle()", chapter.getTitle()) + "}");
602    }
603  146 printer.println();
604  146 if (chapter.getIntroduction() != null && !brief) {
605  146 printer.println(getLatexListEntry("getIntroduction()", chapter.getIntroduction()));
606  146 printer.println();
607    }
608    }
609   
 
610  146 toggle public void visitLeave(final Chapter chapter) {
611  146 printer.println("%% end of chapter " + getLatexListEntry("getTitle()", chapter.getTitle()));
612  146 printer.println();
613  146 setBlocked(false);
614    }
615   
 
616  104 toggle public void visitLeave(final SectionList list) {
617  104 printer.println();
618    }
619   
 
620  280 toggle public void visitEnter(final Section section) {
621    // check if we print only brief and test for non text subnodes
622  280 if (brief) {
623  0 boolean hasFormalContent = false;
624  0 do {
625  0 final SubsectionList subSections = section.getSubsectionList();
626  0 if (subSections == null) {
627  0 break;
628    }
629  0 for (int j = 0; j < subSections.size(); j++) {
630  0 final SubsectionType subSection = subSections.get(j);
631  0 if (!(subSection instanceof Subsection)) {
632  0 hasFormalContent = true;
633  0 break;
634    }
635    }
636    } while (false);
637  0 if (!hasFormalContent) {
638  0 setBlocked(true);
639  0 return;
640    }
641    }
642  280 printer.print("\\section");
643  280 if (section.getNoNumber() != null && section.getNoNumber().booleanValue()) {
644  0 printer.print("*");
645    }
646  280 printer.print("{");
647  280 printer.print(getLatexListEntry("getTitle()", section.getTitle()));
648  280 final String chapterLabel = "chapter" + getCurrentNumbers().getAbsoluteChapterNumber()
649    + "_section" + getCurrentNumbers().getAbsoluteSectionNumber();
650  280 printer.println("} \\label{" + chapterLabel + "} \\hypertarget{" + chapterLabel + "}{}");
651  280 if (section.getIntroduction() != null && !brief) {
652  280 printer.println(getLatexListEntry("getIntroduction()", section.getIntroduction()));
653  280 printer.println();
654    }
655    }
656   
 
657  280 toggle public void visitLeave(final Section section) {
658  280 setBlocked(false);
659    }
660   
 
661  108 toggle public void visitEnter(final Subsection subsection) {
662    /* LATER mime 20070131: use this information?
663    if (subsection.getId() != null) {
664    printer.print(" id=\"" + subsection.getId() + "\"");
665    }
666    if (subsection.getLevel() != null) {
667    printer.print(" level=\"" + subsection.getLevel() + "\"");
668    }
669    */
670  108 if (brief) {
671  0 return;
672    }
673  108 if (subsection.getTitle() != null) {
674  68 printer.print("\\subsection{");
675  68 printer.println(getLatexListEntry("getTitle()", subsection.getTitle()));
676  68 printer.println("}");
677    }
678  108 if (subsection.getId() != null) {
679  4 printer.println("\\label{" + subsection.getId() + "} \\hypertarget{"
680    + subsection.getId() + "}{}");
681    }
682  108 printer.println(getLatexListEntry("getLatex()", subsection.getLatex()));
683    }
684   
 
685  108 toggle public void visitLeave(final Subsection subsection) {
686  108 if (brief) {
687  0 return;
688    }
689  108 printer.println();
690  108 printer.println();
691    }
692   
 
693  992 toggle public void visitEnter(final Node node) {
694    /** TODO mime 20070131: level filter
695    if (node.getLevel() != null) {
696    printer.print(" level=\"" + node.getLevel() + "\"");
697    }
698    */
699  992 if (node.getPrecedingText() != null && !brief) {
700  502 printer.println("\\par");
701  502 printer.println(getLatexListEntry("getPrecedingText()", node.getPrecedingText()));
702  502 printer.println();
703    }
704  992 id = node.getId();
705  992 title = null;
706  992 if (node.getTitle() != null) {
707  552 title = getLatexListEntry("getTitle()", node.getTitle());
708    }
709    }
710   
 
711  992 toggle public void visitLeave(final Node node) {
712  992 printer.println();
713  992 if (node.getSucceedingText() != null && !brief) {
714  144 printer.println(getLatexListEntry("getSucceedingText()", node.getSucceedingText()));
715  144 printer.println();
716    }
717  992 printer.println();
718    }
719   
 
720  236 toggle public void visitEnter(final Axiom axiom) {
721  236 printer.println("\\begin{ax}" + (title != null ? "[" + title + "]" : ""));
722  236 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
723  236 if (info) {
724  236 printer.println("{\\tt \\tiny [\\verb]" + id + "]]}");
725    }
726  236 printFormula(axiom.getFormula().getElement());
727  236 printer.println(getLatexListEntry("getDescription()", axiom.getDescription()));
728  236 printer.println("\\end{ax}");
729    }
730   
 
731  444 toggle public void visitEnter(final Proposition proposition) {
732  444 printer.println("\\begin{prop}" + (title != null ? "[" + title + "]" : ""));
733  444 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
734  444 if (info) {
735  444 printer.println("{\\tt \\tiny [\\verb]" + id + "]]}");
736    }
737  444 printTopFormula(proposition.getFormula().getElement(), id);
738  444 printer.println(getLatexListEntry("getDescription()", proposition.getDescription()));
739  444 printer.println("\\end{prop}");
740    }
741   
 
742  88 toggle public void visitEnter(final Proof proof) {
743    /* LATER mime 20070131: filter level and kind
744    if (proof.getKind() != null) {
745    printer.print(" kind=\"" + proof.getKind() + "\"");
746    }
747    if (proof.getLevel() != null) {
748    printer.print(" level=\"" + proof.getLevel() + "\"");
749    }
750    */
751  88 if (brief) {
752  0 setBlocked(true);
753  0 return;
754    }
755  88 printer.println("\\begin{proof}");
756  88 printer.println(getLatexListEntry("getNonFormalProof()", proof.getNonFormalProof()));
757  88 printer.println("\\end{proof}");
758    }
759   
 
760  88 toggle public void visitLeave(final Proof proof) {
761  88 setBlocked(false);
762    }
763   
 
764  196 toggle public void visitEnter(final FormalProof proof) {
765  196 if (brief) {
766  0 setBlocked(true);
767  0 return;
768    }
769  196 tabLevel = 0;
770  196 printer.println("\\begin{proof}");
771    // if ("de".equals(language)) {
772    // printer.println("Beweis (formal):");
773    // } else {
774    // printer.println("Proof (formal):");
775    // }
776    }
777   
 
778  396 toggle public void visitEnter(final FormalProofLineList lines) {
779  396 if (tabLevel == 0) {
780  196 printer.println("\\mbox{}\\\\");
781  196 printer.println("\\begin{longtable}[h!]{r@{\\extracolsep{\\fill}}p{9cm}@{\\extracolsep{\\fill}}p{4cm}}");
782    }
783    }
784   
 
785  396 toggle public void visitLeave(final FormalProofLineList lines) {
786  396 if (tabLevel == 0) {
787  196 printer.println(" & & \\qedhere");
788  196 printer.println("\\end{longtable}");
789    }
790    }
791   
 
792  2026 toggle public void visitEnter(final FormalProofLine line) {
793  2026 if (line.getLabel() != null) {
794  2022 label = line.getLabel();
795    } else {
796  4 label = "";
797    }
798  2026 if (line.getFormula() != null) {
799  2026 formula = "$" + getQedeqBo().getElement2Latex().getLatex(line.getFormula().getElement()) + "$";
800    } else {
801  0 formula = "";
802    }
803  2026 if (line.getReason() != null) {
804  2026 reason = line.getReason().toString();
805    } else {
806  0 reason = "";
807    }
808    }
809   
 
810  2026 toggle public void visitLeave(final FormalProofLine line) {
811  2026 if (brief) {
812  0 return;
813    }
814  2026 linePrintln();
815    }
816   
817    /**
818    * Print proof line made out of label, formula and reason.
819    */
 
820  2426 toggle private void linePrintln() {
821  2426 if (formula.length() == 0 && reason.length() == 0) {
822  0 return;
823    }
824  2426 if (label.length() > 0) {
825  2422 String display = getNodeBo().getNodeVo().getId() + "!" + label;
826  2422 printer.print("\\label{" + display + "} \\hypertarget{" + display
827    + "}{\\mbox{(" + label + ")}} ");
828    }
829  2426 printer.print(" \\ & \\ ");
830  3494 for (int i = 0; i < tabLevel; i++) {
831  1068 printer.print("\\mbox{\\qquad}");
832    }
833  2426 if (formula.length() > 0) {
834  2426 printer.print(formula);
835    }
836  2426 printer.print(" \\ & \\ ");
837  2426 if (reason.length() > 0) {
838  2426 printer.print("{\\tiny ");
839  2426 printer.print(reason);
840  2426 printer.print("}");
841    }
842  2426 printer.println(" \\\\ ");
843  2426 reason = "";
844  2426 formula = "";
845  2426 label = "";
846    }
847   
 
848  1374 toggle private String getReference(final String reference) {
849  1374 return getReference(reference, "getReference()");
850    }
851   
 
852  2538 toggle private String getReference(final String reference, final String subContext) {
853  2538 final String context = getCurrentContext().getLocationWithinModule();
854  2538 try {
855  2538 getCurrentContext().setLocationWithinModule(context + "." + subContext);
856  2538 return (getReference(reference, null, null));
857    } finally {
858  2538 getCurrentContext().setLocationWithinModule(context);
859    }
860    }
861   
 
862  592 toggle public void visitEnter(final ModusPonens r) throws ModuleDataException {
863  592 if (brief) {
864  0 return;
865    }
866  592 reason = getRuleReference(r.getName());
867  592 boolean one = false;
868  592 if (r.getReference1() != null) {
869  576 reason += " " + getReference(r.getReference1(), "getReference1()");
870  576 one = true;
871    }
872  592 if (r.getReference1() != null) {
873  576 if (one) {
874  576 reason += ",";
875    }
876  576 reason += " " + getReference(r.getReference2(), "getReference2()");
877    }
878    }
879   
 
880  454 toggle public void visitEnter(final Add r) throws ModuleDataException {
881  454 if (brief) {
882  0 return;
883    }
884  454 reason = getRuleReference(r.getName());
885  454 if (r.getReference() != null) {
886  450 reason += " " + getReference(r.getReference());
887    }
888    }
889   
 
890  86 toggle public void visitEnter(final Rename r) throws ModuleDataException {
891  86 if (brief) {
892  0 return;
893    }
894  86 reason = getRuleReference(r.getName());
895  86 if (r.getOriginalSubjectVariable() != null) {
896  74 reason += " $" + getQedeqBo().getElement2Latex().getLatex(
897    r.getOriginalSubjectVariable()) + "$";
898    }
899  86 if (r.getReplacementSubjectVariable() != null) {
900  66 reason += " by $" + getQedeqBo().getElement2Latex().getLatex(
901    r.getReplacementSubjectVariable()) + "$";
902    }
903  86 if (r.getReference() != null) {
904  74 reason += " in " + getReference(r.getReference());
905    }
906    }
907   
 
908  50 toggle public void visitEnter(final SubstFree r) throws ModuleDataException {
909  50 if (brief) {
910  0 return;
911    }
912  50 reason = getRuleReference(r.getName());
913  50 if (r.getSubjectVariable() != null) {
914  34 reason += " $" + getQedeqBo().getElement2Latex().getLatex(
915    r.getSubjectVariable()) + "$";
916    }
917  50 if (r.getSubstituteTerm() != null) {
918  46 reason += " by $" + getQedeqBo().getElement2Latex().getLatex(
919    r.getSubstituteTerm()) + "$";
920    }
921  50 if (r.getReference() != null) {
922  46 reason += " in " + getReference(r.getReference());
923    }
924    }
925   
 
926  16 toggle public void visitEnter(final SubstFunc r) throws ModuleDataException {
927  16 if (brief) {
928  0 return;
929    }
930  16 reason = getRuleReference(r.getName());
931  16 if (r.getFunctionVariable() != null) {
932  8 reason += " $" + getQedeqBo().getElement2Latex().getLatex(
933    r.getFunctionVariable()) + "$";
934    }
935  16 if (r.getSubstituteTerm() != null) {
936  12 reason += " by $" + getQedeqBo().getElement2Latex().getLatex(
937    r.getSubstituteTerm()) + "$";
938    }
939  16 if (r.getReference() != null) {
940  12 reason += " in " + getReference(r.getReference());
941    }
942    }
943   
 
944  778 toggle public void visitEnter(final SubstPred r) throws ModuleDataException {
945  778 if (brief) {
946  0 return;
947    }
948  778 reason = getRuleReference(r.getName());
949  778 if (r.getPredicateVariable() != null) {
950  742 reason += " $" + getQedeqBo().getElement2Latex().getLatex(
951    r.getPredicateVariable()) + "$";
952    }
953  778 if (r.getSubstituteFormula() != null) {
954  742 reason += " by $" + getQedeqBo().getElement2Latex().getLatex(
955    r.getSubstituteFormula()) + "$";
956    }
957  778 if (r.getReference() != null) {
958  746 reason += " in " + getReference(r.getReference());
959    }
960    }
961   
 
962  10 toggle public void visitEnter(final Existential r) throws ModuleDataException {
963  10 if (brief) {
964  0 return;
965    }
966  10 reason = getRuleReference(r.getName());
967  10 if (r.getSubjectVariable() != null) {
968  6 reason += " with $" + getQedeqBo().getElement2Latex().getLatex(
969    r.getSubjectVariable()) + "$";
970    }
971  10 if (r.getReference() != null) {
972  10 reason += " in " + getReference(r.getReference());
973    }
974    }
975   
 
976  40 toggle public void visitEnter(final Universal r) throws ModuleDataException {
977  40 if (brief) {
978  0 return;
979    }
980  40 reason = getRuleReference(r.getName());
981  40 if (r.getSubjectVariable() != null) {
982  28 reason += " with $" + getQedeqBo().getElement2Latex().getLatex(
983    r.getSubjectVariable()) + "$";
984    }
985  40 if (r.getReference() != null) {
986  36 reason += " in " + getReference(r.getReference());
987    }
988    }
989   
 
990  200 toggle public void visitEnter(final ConditionalProof r) throws ModuleDataException {
991  200 if (brief) {
992  0 return;
993    }
994  200 reason = getRuleReference(r.getName());
995  200 printer.print(" \\ & \\ ");
996  304 for (int i = 0; i < tabLevel; i++) {
997  104 printer.print("\\mbox{\\qquad}");
998    }
999  200 printer.println("Conditional Proof");
1000  200 printer.print(" \\ & \\ ");
1001  200 printer.println(" \\\\ ");
1002  200 tabLevel++;
1003    }
1004   
 
1005  200 toggle public void visitLeave(final ConditionalProof proof) {
1006  200 if (brief) {
1007  0 return;
1008    }
1009  200 tabLevel--;
1010    }
1011   
 
1012  200 toggle public void visitEnter(final Hypothesis hypothesis) {
1013  200 if (brief) {
1014  0 return;
1015    }
1016  200 reason = "Hypothesis";
1017  200 if (hypothesis.getLabel() != null) {
1018  200 label = hypothesis.getLabel();
1019    }
1020  200 if (hypothesis.getFormula() != null) {
1021  200 formula = "$" + getQedeqBo().getElement2Latex().getLatex(
1022    hypothesis.getFormula().getElement()) + "$";
1023    }
1024    }
1025   
 
1026  200 toggle public void visitLeave(final Hypothesis hypothesis) {
1027  200 if (brief) {
1028  0 return;
1029    }
1030  200 linePrintln();
1031    }
1032   
 
1033  200 toggle public void visitEnter(final Conclusion conclusion) {
1034  200 if (brief) {
1035  0 return;
1036    }
1037  200 tabLevel--;
1038  200 reason = "Conclusion";
1039  200 if (conclusion.getLabel() != null) {
1040  200 label = conclusion.getLabel();
1041    }
1042  200 if (conclusion.getFormula() != null) {
1043  200 formula = "$" + getQedeqBo().getElement2Latex().getLatex(
1044    conclusion.getFormula().getElement()) + "$";
1045    }
1046    }
1047   
 
1048  200 toggle public void visitLeave(final Conclusion conclusion) {
1049  200 if (brief) {
1050  0 return;
1051    }
1052  200 linePrintln();
1053  200 tabLevel++;
1054    }
1055   
 
1056  196 toggle public void visitLeave(final FormalProof proof) {
1057  196 if (!getBlocked()) {
1058  196 printer.println("\\end{proof}");
1059    }
1060  196 setBlocked(false);
1061    }
1062   
 
1063  20 toggle public void visitEnter(final InitialPredicateDefinition definition) {
1064  20 printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : ""));
1065  20 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
1066  20 if (info) {
1067  20 printer.println("{\\tt \\tiny [\\verb]" + id + "]]}");
1068    }
1069  20 printer.print("$$");
1070  20 printer.println(getLatex(definition.getPredCon()));
1071  20 printer.println("$$");
1072  20 printer.println(getLatexListEntry("getDescription()", definition.getDescription()));
1073  20 printer.println("\\end{idefn}");
1074    }
1075   
 
1076  48 toggle public void visitEnter(final PredicateDefinition definition) {
1077  48 printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : ""));
1078  48 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
1079  48 if (info) {
1080  48 printer.println("{\\tt \\tiny [\\verb]" + id + "]]}");
1081    }
1082  48 printer.print("$$");
1083  48 printer.print(getLatex(definition.getFormula().getElement()));
1084  48 printer.println("$$");
1085  48 printer.println(getLatexListEntry("getDescription()", definition.getDescription()));
1086  48 printer.println("\\end{defn}");
1087    }
1088   
 
1089  0 toggle public void visitEnter(final InitialFunctionDefinition definition) {
1090  0 printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : ""));
1091  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
1092  0 if (info) {
1093  0 printer.println("{\\tt \\tiny [\\verb]" + id + "]]}");
1094    }
1095  0 printer.print("$$");
1096  0 printer.print(getLatex(definition.getFunCon()));
1097  0 printer.println("$$");
1098  0 printer.println(getLatexListEntry("getDescription()", definition.getDescription()));
1099  0 printer.println("\\end{defn}");
1100    }
1101   
 
1102  64 toggle public void visitEnter(final FunctionDefinition definition) {
1103  64 printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : ""));
1104  64 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
1105  64 if (info) {
1106  64 printer.println("{\\tt \\tiny [\\verb]" + id + "]]}");
1107    }
1108  64 printer.print("$$");
1109  64 printer.print(getLatex(definition.getFormula().getElement()));
1110  64 printer.println("$$");
1111  64 printer.println("\\end{defn}");
1112    }
1113   
 
1114  64 toggle public void visitLeave(final FunctionDefinition definition) {
1115    // nothing to do
1116    }
1117   
 
1118  180 toggle public void visitEnter(final Rule rule) {
1119  180 printer.println("\\begin{rul}" + (title != null ? "[" + title + "]" : ""));
1120  180 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
1121  180 if (info) {
1122  180 printer.println("{\\tt \\tiny [\\verb]" + id + "]]}");
1123    }
1124  180 printer.println();
1125  180 printer.println("\\par");
1126  180 printer.println("{\\em "
1127  180 + (rule.getName() != null ? " Name: \\verb]" + rule.getName() + "]" : "")
1128  180 + (rule.getVersion() != null ? " - Version: \\verb]" + rule.getVersion() + "]" : "")
1129    + "}");
1130  180 printer.println();
1131  180 printer.println();
1132  180 printer.println(getLatexListEntry("getDescription()", rule.getDescription()));
1133  180 printer.println("\\end{rul}");
1134    }
1135   
 
1136  180 toggle public void visitLeave(final Rule rule) {
1137    // nothing to do
1138    }
1139   
 
1140  8 toggle public void visitEnter(final LinkList linkList) {
1141  8 if (linkList.size() <= 0) {
1142  0 return;
1143    }
1144  8 if ("de".equals(language)) {
1145  4 printer.println("Basierend auf: ");
1146    } else {
1147  4 if (!"en".equals(language)) {
1148  0 printer.println("%%% TODO unknown language: " + language);
1149    }
1150  4 printer.println("Based on: ");
1151    }
1152  20 for (int i = 0; i < linkList.size(); i++) {
1153  12 if (linkList.get(i) != null) {
1154  12 printer.print(" " + getReference(linkList.get(i), "get(" + i + ")"));
1155    }
1156  8 };
1157  8 printer.println();
1158    }
1159   
 
1160  4 toggle public void visitEnter(final ChangedRuleList list) {
1161  4 if (list.size() <= 0) {
1162  0 return;
1163    }
1164  4 if ("de".equals(language)) {
1165  2 printer.println("Die folgenden Regeln m\u00fcssen erweitert werden.");
1166    } else {
1167  2 if (!"en".equals(language)) {
1168  0 printer.println("%%% TODO unknown language: " + language);
1169    }
1170  2 printer.println("The following rules have to be extended.");
1171    }
1172  4 printer.println();
1173    }
1174   
 
1175  32 toggle public void visitEnter(final ChangedRule rule) {
1176  32 printer.println("\\par");
1177  32 printer.println("\\label{" + id + "!" + rule.getName() + "} \\hypertarget{" + id + "!"
1178    + rule.getName() + "}{}");
1179  32 printer.print("{\\em "
1180  32 + (rule.getName() != null ? " Name: \\verb]" + rule.getName() + "]" : "")
1181  32 + (rule.getVersion() != null ? " - Version: \\verb]" + rule.getVersion() + "]" : ""));
1182  32 RuleKey old = getLocalRuleKey(rule.getName());
1183  32 if (old == null && getQedeqBo().getExistenceChecker() != null) {
1184  0 old = getQedeqBo().getExistenceChecker().getParentRuleKey(rule.getName());
1185    }
1186  32 if (old != null) {
1187  32 printer.print(" - Old Version: "
1188    + getRuleReference(rule.getName(), old.getVersion()));
1189    }
1190  32 printer.println("}");
1191  32 rule.getName();
1192  32 printer.println();
1193  32 if (rule.getDescription() != null) {
1194  32 printer.println(getLatexListEntry("getDescription()", rule.getDescription()));
1195  32 printer.println();
1196  32 printer.println();
1197    }
1198    }
1199   
1200   
 
1201  14 toggle public void visitEnter(final LiteratureItemList list) {
1202  14 printer.println("\\backmatter");
1203  14 printer.println();
1204  14 printer.println("\\begin{thebibliography}{99}");
1205  14 if ("de".equals(language)) {
1206  6 printer.println("\\addcontentsline{toc}{chapter}{Literaturverzeichnis}");
1207    } else {
1208  8 if (!"en".equals(language)) {
1209  0 printer.println("%%% TODO unknown language: " + language);
1210    }
1211  8 printer.println("\\addcontentsline{toc}{chapter}{Bibliography}");
1212    }
1213  14 final ImportList imports = getQedeqBo().getQedeq().getHeader().getImportList();
1214  14 if (imports != null && imports.size() > 0) {
1215  6 printer.println();
1216  6 printer.println();
1217  6 printer.println("%% Used other QEDEQ modules:");
1218  14 for (int i = 0; i < imports.size(); i++) {
1219  8 final Import imp = imports.get(i);
1220  8 printer.print("\\bibitem{" + imp.getLabel() + "} ");
1221  8 final Specification spec = imp.getSpecification();
1222  8 printer.print(getLatex(spec.getName()));
1223  8 if (spec.getLocationList() != null && spec.getLocationList().size() > 0
1224    && spec.getLocationList().get(0).getLocation().length() > 0) {
1225  8 printer.print(" ");
1226    // TODO m31 20070205, 2010727: later on here must stand the location that was used
1227    // to verify the document contents.
1228    // Also get other informations like authors, title, etc.
1229    // It might also be better to link to URL?
1230    // printer.print("\\url{" + getUrl(getQedeqBo().getModuleAddress(), spec) + "}");
1231  8 printer.print("\\url{" + getPdfLink((KernelQedeqBo) getQedeqBo()
1232    .getLabels().getReferences().getQedeqBo(imp.getLabel())) + "}");
1233    }
1234  8 printer.println();
1235    }
1236  6 printer.println();
1237  6 printer.println();
1238  6 printer.println("%% Other references:");
1239  6 printer.println();
1240    }
1241    }
1242   
 
1243  14 toggle public void visitLeave(final LiteratureItemList list) {
1244  14 final UsedByList usedby = getQedeqBo().getQedeq().getHeader().getUsedByList();
1245  14 if (usedby != null && usedby.size() > 0) {
1246  8 printer.println();
1247  8 printer.println();
1248  8 printer.println("%% QEDEQ modules that use this one:");
1249  16 for (int i = 0; i < usedby.size(); i++) {
1250  8 final Specification spec = usedby.get(i);
1251  8 printer.print("\\bibitem{" + spec.getName() + "} ");
1252  8 printer.print(getLatex(spec.getName()));
1253  8 final String url = getUrl(getQedeqBo().getModuleAddress(), spec);
1254  8 if (url != null && url.length() > 0) {
1255  8 printer.print(" ");
1256  8 printer.print("\\url{" + url + "}");
1257    }
1258  8 printer.println();
1259    }
1260  8 printer.println();
1261  8 printer.println();
1262    }
1263  14 printer.println("\\end{thebibliography}");
1264    }
1265   
 
1266  56 toggle public void visitEnter(final LiteratureItem item) {
1267  56 printer.print("\\bibitem{" + item.getLabel() + "} ");
1268  56 printer.println(getLatexListEntry("getItem()", item.getItem()));
1269  56 printer.println();
1270    }
1271   
1272    /**
1273    * Print top level formula. If the formula has the form <code>AND(.., .., ..)</code> the
1274    * formula is broken down in several labeled lines.
1275    *
1276    * @param element Formula to print.
1277    * @param mainLabel Main formula label.
1278    */
 
1279  444 toggle private void printTopFormula(final Element element, final String mainLabel) {
1280  444 if (!element.isList() || !element.getList().getOperator().equals("AND")) {
1281  372 printFormula(element);
1282  372 return;
1283    }
1284  72 final ElementList list = element.getList();
1285  72 printer.println("\\mbox{}");
1286  72 printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{0.9\\linewidth}l}}");
1287  608 for (int i = 0; i < list.size(); i++) {
1288  536 String newLabel = "";
1289  536 if (list.size() >= ALPHABET.length() * ALPHABET.length()) {
1290  0 newLabel = "" + (i + 1);
1291    } else {
1292    // TODO 20110303 m31: this dosn't work if we have more than 26 * 26 elements
1293  536 if (list.size() > ALPHABET.length()) {
1294  160 final int div = (i / ALPHABET.length());
1295  160 newLabel = "" + ALPHABET.charAt(div);
1296    }
1297  536 newLabel += ALPHABET.charAt(i % ALPHABET.length());
1298    }
1299    // final String label = (i < ALPHABET.length() ? "" + ALPHABET .charAt(i) : "" + i);
1300  536 printer.println("\\centering $" + getLatex(list.getElement(i)) + "$"
1301    + " & \\label{" + mainLabel + "/" + newLabel + "} \\hypertarget{" + mainLabel + "/"
1302    + newLabel + "}{} \\mbox{\\emph{(" + newLabel + ")}} "
1303  536 + (i + 1 < list.size() ? "\\\\" : ""));
1304    }
1305  72 printer.println("\\end{longtable}");
1306    }
1307   
1308    /**
1309    * Print formula.
1310    *
1311    * @param element Formula to print.
1312    */
 
1313  608 toggle private void printFormula(final Element element) {
1314  608 printer.println("\\mbox{}");
1315  608 printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{\\linewidth}}}");
1316  608 printer.println("\\centering $" + getLatex(element) + "$");
1317  608 printer.println("\\end{longtable}");
1318    }
1319   
1320    /**
1321    * Get LaTeX element presentation.
1322    *
1323    * @param element Print this element.
1324    * @return LaTeX form of element.
1325    */
 
1326  1276 toggle private String getLatex(final Element element) {
1327  1276 return getQedeqBo().getElement2Latex().getLatex(element);
1328    }
1329   
1330    /**
1331    * Filters correct entry out of LaTeX list. Filter criterion is for example the correct
1332    * language.
1333    * TODO mime 20050205: filter level too?
1334    *
1335    * @param method This method was called. Used to get the correct sub context.
1336    * Should not be null. If it is empty the <code>subContext</code>
1337    * is not changed.
1338    * @param list List of LaTeX texts.
1339    * @return Filtered text.
1340    */
 
1341  3556 toggle private String getLatexListEntry(final String method, final LatexList list) {
1342  3556 if (list == null) {
1343  744 return "";
1344    }
1345  2812 if (method.length() > 0) {
1346  2812 subContext = method;
1347    }
1348  2812 try {
1349  4024 for (int i = 0; language != null && i < list.size(); i++) {
1350  3812 if (language.equals(list.get(i).getLanguage())) {
1351  2600 if (method.length() > 0) {
1352  2600 subContext = method + ".get(" + i + ")";
1353    }
1354  2600 return getLatex(list.get(i));
1355    }
1356    }
1357    // OK, we didn't found the language, so we take the default language
1358  212 final String def = getQedeqBo().getOriginalLanguage();
1359  232 for (int i = 0; i < list.size(); i++) {
1360  212 if (EqualsUtility.equals(def, list.get(i).getLanguage())) {
1361  192 if (method.length() > 0) {
1362  192 subContext = method + ".get(" + i + ")";
1363    }
1364  192 return "MISSING! OTHER: " + getLatex(list.get(i));
1365    }
1366    }
1367    // OK, we didn't find wanted and default language, so we take the first non empty one
1368  22 for (int i = 0; i < list.size(); i++) {
1369  20 if (method.length() > 0) {
1370  20 subContext = method + ".get(" + i + ")";
1371    }
1372  20 if (null != list.get(i) && null != list.get(i).getLatex()
1373    && list.get(i).getLatex().trim().length() > 0) {
1374  18 return "MISSING! OTHER: " + getLatex(list.get(i));
1375    }
1376    }
1377  2 return "MISSING!";
1378    } finally {
1379  2812 if (method.length() > 0) {
1380  2812 subContext = "";
1381    }
1382    }
1383    }
1384   
1385    /**
1386    * Get really LaTeX. Does some simple character replacements for umlauts. Also transforms
1387    * <code>\qref{key}</code> into LaTeX.
1388    *
1389    * @param latex Unescaped text.
1390    * @return Really LaTeX.
1391    */
 
1392  2810 toggle private String getLatex(final Latex latex) {
1393  2810 if (latex == null || latex.getLatex() == null) {
1394  6 return "";
1395    }
1396  2804 StringBuffer result = new StringBuffer(latex.getLatex());
1397   
1398    // LATER mime 20080324: check if LaTeX is correct and no forbidden tags are used
1399   
1400  2804 transformQref(result);
1401   
1402  2804 return deleteLineLeadingWhitespace(result.toString());
1403    }
1404   
1405    /**
1406    * Transform <code>\qref{key}</code> entries into common LaTeX code.
1407    *
1408    * LATER mime 20080324: write JUnitTests to be sure that no runtime exceptions are thrown if
1409    * reference is at end of latex etc.
1410    *
1411    * @param result Work on this buffer.
1412    */
 
1413  2804 toggle private void transformQref(final StringBuffer result) {
1414  2804 final String method = "transformQref(StringBuffer)";
1415  2804 final StringBuffer buffer = new StringBuffer(result.toString());
1416  2804 final TextInput input = new TextInput(buffer);
1417  2804 int last = 0;
1418  2804 try {
1419  2804 result.setLength(0);
1420  3273 while (input.forward("\\qref{")) {
1421  469 final SourcePosition startPosition = input.getSourcePosition();
1422  469 final int start = input.getPosition();
1423  469 if (!input.forward("}")) {
1424  0 addWarning(LatexErrorCodes.QREF_END_NOT_FOUND_CODE,
1425    LatexErrorCodes.QREF_END_NOT_FOUND_TEXT, startPosition,
1426    input.getSourcePosition());
1427  0 continue;
1428    }
1429  469 String ref = input.getSubstring(start + "\\qref{".length(), input.getPosition()).trim();
1430  469 input.read(); // read }
1431  469 Trace.param(CLASS, this, method, "1 ref", ref);
1432  469 if (ref.length() == 0) {
1433  1 addWarning(LatexErrorCodes.QREF_EMPTY_CODE, LatexErrorCodes.QREF_EMPTY_TEXT,
1434    startPosition, input.getSourcePosition());
1435  1 continue;
1436    }
1437  468 if (ref.length() > 1024) {
1438  0 addWarning(LatexErrorCodes.QREF_END_NOT_FOUND_CODE,
1439    LatexErrorCodes.QREF_END_NOT_FOUND_TEXT, startPosition,
1440    input.getSourcePosition());
1441  0 continue;
1442    }
1443  468 if (ref.indexOf("{") >= 0) {
1444  1 addWarning(LatexErrorCodes.QREF_END_NOT_FOUND_CODE,
1445    LatexErrorCodes.QREF_END_NOT_FOUND_TEXT, startPosition,
1446    input.getSourcePosition());
1447  1 continue;
1448    }
1449  467 final int end = input.getPosition();
1450  467 final SourcePosition endPosition = input.getSourcePosition();
1451  467 result.append(buffer.substring(last, start));
1452  467 result.append(getReference(ref, startPosition, endPosition));
1453  467 last = end;
1454    }
1455    } finally { // thanks to findbugs
1456  2804 IoUtility.close(input);
1457  2804 if (last < buffer.length()) {
1458  2804 result.append(buffer.substring(last));
1459    }
1460    }
1461    }
1462   
 
1463  3005 toggle private String getReference(final String reference, final SourcePosition start, final SourcePosition end) {
1464  3005 final String method = "getReference(String, String)";
1465  3005 Trace.param(CLASS, this, method, "2 reference", reference); // qreference within module
1466   
1467  3005 final Reference ref = getReference(reference, getCurrentContext(start, end), true, false);
1468  3005 if (ref.isNodeLocalReference() && ref.isSubReference()) {
1469  0 return "\\hyperlink{" + ref.getNodeLabel() + "/" + ref.getSubLabel() + "}{" + "("
1470    + ref.getSubLabel() + ")" + "}";
1471    }
1472   
1473  3005 if (ref.isNodeLocalReference() && ref.isProofLineReference()) {
1474  2052 return "\\hyperlink{" + ref.getNodeLabel() + "!" + ref.getProofLineLabel() + "}{" + "("
1475    + ref.getProofLineLabel() + ")" + "}";
1476    }
1477   
1478  953 if (!ref.isExternal()) {
1479  804 return "\\hyperlink{" + ref.getNodeLabel()
1480  804 + (ref.isSubReference() ? "/" + ref.getSubLabel() : "")
1481  804 + (ref.isProofLineReference() ? "!" + ref.getProofLineLabel() : "")
1482    + "}{"
1483    + getNodeDisplay(ref.getNodeLabel(), ref.getNode())
1484  804 + (ref.isSubReference() ? " (" + ref.getSubLabel() + ")" : "")
1485  804 + (ref.isProofLineReference() ? " (" + ref.getProofLineLabel() + ")" : "")
1486    + "}";
1487    }
1488   
1489    // do we have an external module reference without node?
1490  149 if (ref.isExternalModuleReference()) {
1491  8 return "\\url{" + getPdfLink(ref.getExternalQedeq()) + "}~\\cite{"
1492    + ref.getExternalQedeqLabel() + "}";
1493    // if we want to show the text "description": \href{my_url}{description}
1494    }
1495   
1496  141 String external = getPdfLink(ref.getExternalQedeq());
1497  141 if (external.startsWith("file://")) {
1498  1 external = "file:" + external.substring("file://".length());
1499    }
1500  141 return "\\hyperref{" + external + "}{}{"
1501    + ref.getNodeLabel()
1502  141 + (ref.isSubReference() ? "/" + ref.getSubLabel() : "")
1503  141 + (ref.isProofLineReference() ? "!" + ref.getProofLineLabel() : "")
1504    + "}{" + getNodeDisplay(ref.getNodeLabel(), ref.getNode())
1505  141 + (ref.isSubReference() ? " (" + ref.getSubLabel() + ")" : "")
1506  141 + (ref.isProofLineReference() ? " (" + ref.getProofLineLabel() + ")" : "")
1507    + "}~\\cite{" + ref.getExternalQedeqLabel() + "}";
1508    }
1509   
 
1510  945 toggle private String getNodeDisplay(final String label, final KernelNodeBo kNode) {
1511  945 return StringUtility.replace(getNodeDisplay(label, kNode, language), " ", "~");
1512    }
1513   
 
1514  2226 toggle private String getRuleReference(final String ruleName) {
1515  2226 return getRuleReference(ruleName, ruleName);
1516    }
1517   
 
1518  2258 toggle private String getRuleReference(final String ruleName, final String caption) {
1519  2258 final String method = "getRuleReference(String, String)";
1520  2258 Trace.param(CLASS, this, method, "ruleName", ruleName);
1521  2258 RuleKey key = getLocalRuleKey(ruleName);
1522  2258 if (key == null && getQedeqBo().getExistenceChecker() != null) {
1523  0 key = getQedeqBo().getExistenceChecker().getParentRuleKey(ruleName);
1524    }
1525  2258 if (key == null) {
1526  0 key = getQedeqBo().getLabels().getRuleKey(ruleName);
1527    }
1528  2258 KernelQedeqBo qedeq = getQedeqBo();
1529  2258 if (getQedeqBo().getExistenceChecker() != null) {
1530  2258 qedeq = getQedeqBo().getExistenceChecker().getQedeq(key);
1531    }
1532  2258 String localRef = getQedeqBo().getLabels().getRuleLabel(key);
1533  2258 final String refRuleName = qedeq.getLabels().getRule(key).getName();
1534  2258 if (!ruleName.equals(refRuleName)) {
1535  1256 localRef += "!" + ruleName;
1536    }
1537  2258 qedeq.getLabels().getRule(key).getName();
1538  2258 boolean local = getQedeqBo().equals(qedeq);
1539  2258 if (local) {
1540  2258 return "\\hyperlink{" + localRef + "}{" + caption + "}";
1541    }
1542  0 String external = getPdfLink(qedeq);
1543  0 if (external.startsWith("file://")) {
1544  0 external = "file:" + external.substring("file://".length());
1545    }
1546  0 return "\\hyperref{" + external + "}{}{" + caption + "}{"
1547    + localRef + "}";
1548    }
1549   
1550    /**
1551    * Get current module context. Uses sub context information.
1552    *
1553    * @param startDelta Skip position (relative to location start). Could be
1554    * <code>null</code>.
1555    * @param endDelta Mark until this column (relative to location start).
1556    * be <code>null</code>
1557    * @return Current module context.
1558    */
 
1559  3007 toggle public ModuleContext getCurrentContext(final SourcePosition startDelta,
1560    final SourcePosition endDelta) {
1561  3007 if (subContext.length() == 0) {
1562  2538 return super.getCurrentContext();
1563    }
1564  469 final ModuleContext c = new ModuleContext(super.getCurrentContext().getModuleLocation(),
1565    super.getCurrentContext().getLocationWithinModule() + "." + subContext,
1566    startDelta, endDelta);
1567  469 return c;
1568    }
1569   
1570    // TODO 20110214 m31: decide about removal
1571    // public ModuleContext getCurrentContext() {
1572    // throw new IllegalStateException("programming error");
1573    // }
1574   
1575   
1576    /**
1577    * Add warning.
1578    *
1579    * @param code Warning code.
1580    * @param msg Warning message.
1581    * @param startDelta Skip position (relative to location start). Could be
1582    * <code>null</code>.
1583    * @param endDelta Mark until this column (relative to location start).
1584    * be <code>null</code>
1585    */
 
1586  2 toggle private void addWarning(final int code, final String msg, final SourcePosition startDelta,
1587    final SourcePosition endDelta) {
1588  2 Trace.param(CLASS, this, "addWarning", "msg", msg);
1589  2 addWarning(new LatexContentException(code, msg, getCurrentContext(startDelta, endDelta)));
1590    }
1591   
1592    /**
1593    * Get URL to for PDF version of module. If the referenced module doesn't
1594    * support the current language we switch to the original language.
1595    *
1596    * @param prop Get URL for this QEDEQ module.
1597    * @return URL to PDF.
1598    */
 
1599  189 toggle private String getPdfLink(final KernelQedeqBo prop) {
1600  189 if (prop == null) {
1601  4 return "";
1602    }
1603  185 final String url = prop.getUrl();
1604  185 final int dot = url.lastIndexOf(".");
1605  185 if (prop.isSupportedLanguage(language)) {
1606  185 return url.substring(0, dot) + "_" + language + ".pdf";
1607    }
1608  0 final String a = prop.getOriginalLanguage();
1609  0 return url.substring(0, dot) + (a.length() > 0 ? "_" + a : "") + ".pdf";
1610    }
1611   
1612    /**
1613    * Get LaTeX from string. Escapes common characters.
1614    * Also gets rid of leading spaces if they are equal among the lines.
1615    *
1616    * @param text Unescaped text.
1617    * @return LaTeX.
1618    */
 
1619  48 toggle private String getLatex(final String text) {
1620  48 final StringBuffer buffer = new StringBuffer(text);
1621  48 StringUtility.replace(buffer, "\\", "\\textbackslash");
1622  48 StringUtility.replace(buffer, "$", "\\$");
1623  48 StringUtility.replace(buffer, "&", "\\&");
1624  48 StringUtility.replace(buffer, "%", "\\%");
1625  48 StringUtility.replace(buffer, "#", "\\#");
1626  48 StringUtility.replace(buffer, "_", "\\_");
1627  48 StringUtility.replace(buffer, "{", "\\{");
1628  48 StringUtility.replace(buffer, "}", "\\}");
1629  48 StringUtility.replace(buffer, "~", "\\textasciitilde");
1630  48 StringUtility.replace(buffer, "^", "\\textasciicircum");
1631  48 StringUtility.replace(buffer, "<", "\\textless");
1632  48 StringUtility.replace(buffer, ">", "\\textgreater");
1633  48 StringUtility.deleteLineLeadingWhitespace(buffer);
1634  48 return buffer.toString().trim();
1635    }
1636   
1637    /**
1638    * Trims text. Also gets rid of leading spaces if they are equal among the lines.
1639    *
1640    * @param text Text.
1641    * @return Untrimed text.
1642    */
 
1643  2804 toggle private String deleteLineLeadingWhitespace(final String text) {
1644  2804 final StringBuffer buffer = new StringBuffer(text);
1645  2804 StringUtility.deleteLineLeadingWhitespace(buffer);
1646  2804 return buffer.toString().trim();
1647    }
1648   
1649    /**
1650    * Get really LaTeX. Does some simple character replacements for umlauts.
1651    * LATER mime 20050205: filter more than German umlauts
1652    *
1653    * @param nearlyLatex Unescaped text.
1654    * @return Really LaTeX.
1655    */
 
1656  533220 toggle private String escapeUmlauts(final String nearlyLatex) {
1657  533220 if (nearlyLatex == null) {
1658  0 return "";
1659    }
1660  533220 final StringBuffer buffer = new StringBuffer(nearlyLatex);
1661    // System.out.println("before");
1662    // System.out.println(buffer);
1663    // System.out.println();
1664    // System.out.println("after");
1665    // System.out.println(buffer);
1666    // System.out.println("*******************************************************************");
1667  533220 StringUtility.replace(buffer, "\u00fc", "{\\\"u}");
1668  533220 StringUtility.replace(buffer, "\u00f6", "{\\\"o}");
1669  533220 StringUtility.replace(buffer, "\u00e4", "{\\\"a}");
1670  533220 StringUtility.replace(buffer, "\u00dc", "{\\\"U}");
1671  533220 StringUtility.replace(buffer, "\u00d6", "{\\\"O}");
1672  533220 StringUtility.replace(buffer, "\u00c4", "{\\\"A}");
1673  533220 StringUtility.replace(buffer, "\u00df", "{\\ss}");
1674  533220 return buffer.toString();
1675    }
1676   
1677    }
 
CloverReport generated by Clover Code Coverage v3.1.10
Fri May 24 2013 13:47:32 UTC.		   Clover: Open Source License registered to qedeq.org .