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
649   1,372   269   9.27
334   1,089   0.41   70
70     3.84  
1    
 
  Qedeq2UnicodeVisitor       Line # 98 649 269 77.8% 0.7777778
 
  (9)
 
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.unicode;
17   
18    import java.io.IOException;
19    import java.util.ArrayList;
20    import java.util.List;
21   
22    import org.apache.commons.lang.ArrayUtils;
23    import org.qedeq.base.io.AbstractOutput;
24    import org.qedeq.base.io.SourcePosition;
25    import org.qedeq.base.io.TextOutput;
26    import org.qedeq.base.trace.Trace;
27    import org.qedeq.base.utility.DateUtility;
28    import org.qedeq.base.utility.EqualsUtility;
29    import org.qedeq.base.utility.StringUtility;
30    import org.qedeq.kernel.bo.module.ControlVisitor;
31    import org.qedeq.kernel.bo.module.InternalServiceProcess;
32    import org.qedeq.kernel.bo.module.KernelNodeBo;
33    import org.qedeq.kernel.bo.module.KernelQedeqBo;
34    import org.qedeq.kernel.bo.module.Reference;
35    import org.qedeq.kernel.se.base.list.Element;
36    import org.qedeq.kernel.se.base.list.ElementList;
37    import org.qedeq.kernel.se.base.module.Add;
38    import org.qedeq.kernel.se.base.module.Author;
39    import org.qedeq.kernel.se.base.module.AuthorList;
40    import org.qedeq.kernel.se.base.module.Axiom;
41    import org.qedeq.kernel.se.base.module.ChangedRule;
42    import org.qedeq.kernel.se.base.module.ChangedRuleList;
43    import org.qedeq.kernel.se.base.module.Chapter;
44    import org.qedeq.kernel.se.base.module.Conclusion;
45    import org.qedeq.kernel.se.base.module.ConditionalProof;
46    import org.qedeq.kernel.se.base.module.Existential;
47    import org.qedeq.kernel.se.base.module.FormalProof;
48    import org.qedeq.kernel.se.base.module.FormalProofLine;
49    import org.qedeq.kernel.se.base.module.Formula;
50    import org.qedeq.kernel.se.base.module.FunctionDefinition;
51    import org.qedeq.kernel.se.base.module.Header;
52    import org.qedeq.kernel.se.base.module.Hypothesis;
53    import org.qedeq.kernel.se.base.module.Import;
54    import org.qedeq.kernel.se.base.module.ImportList;
55    import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
56    import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
57    import org.qedeq.kernel.se.base.module.Latex;
58    import org.qedeq.kernel.se.base.module.LatexList;
59    import org.qedeq.kernel.se.base.module.LinkList;
60    import org.qedeq.kernel.se.base.module.LiteratureItem;
61    import org.qedeq.kernel.se.base.module.LiteratureItemList;
62    import org.qedeq.kernel.se.base.module.LocationList;
63    import org.qedeq.kernel.se.base.module.ModusPonens;
64    import org.qedeq.kernel.se.base.module.Node;
65    import org.qedeq.kernel.se.base.module.PredicateDefinition;
66    import org.qedeq.kernel.se.base.module.Proof;
67    import org.qedeq.kernel.se.base.module.Proposition;
68    import org.qedeq.kernel.se.base.module.Qedeq;
69    import org.qedeq.kernel.se.base.module.Rename;
70    import org.qedeq.kernel.se.base.module.Rule;
71    import org.qedeq.kernel.se.base.module.Section;
72    import org.qedeq.kernel.se.base.module.SectionList;
73    import org.qedeq.kernel.se.base.module.Specification;
74    import org.qedeq.kernel.se.base.module.Subsection;
75    import org.qedeq.kernel.se.base.module.SubsectionList;
76    import org.qedeq.kernel.se.base.module.SubsectionType;
77    import org.qedeq.kernel.se.base.module.SubstFree;
78    import org.qedeq.kernel.se.base.module.SubstFunc;
79    import org.qedeq.kernel.se.base.module.SubstPred;
80    import org.qedeq.kernel.se.base.module.Universal;
81    import org.qedeq.kernel.se.base.module.UsedByList;
82    import org.qedeq.kernel.se.common.ModuleAddress;
83    import org.qedeq.kernel.se.common.ModuleContext;
84    import org.qedeq.kernel.se.common.ModuleDataException;
85    import org.qedeq.kernel.se.common.Plugin;
86    import org.qedeq.kernel.se.common.SourceFileExceptionList;
87    import org.qedeq.kernel.se.visitor.QedeqNumbers;
88   
89   
90    /**
91    * Transfer a QEDEQ module into unicode text.
92    * <p>
93    * <b>This is just a quick written generator. This class just generates some text output to be able
94    * to get a visual impression of a QEDEQ module.</b>
95    *
96    * @author Michael Meyling
97    */
 
98    public class Qedeq2UnicodeVisitor extends ControlVisitor implements ReferenceFinder {
99   
100    /** This class. */
101    private static final Class CLASS = Qedeq2UnicodeVisitor.class;
102   
103    /** Output goes here. */
104    private AbstractOutput printer;
105   
106    /** Filter text to get and produce text in this language. */
107    private String language;
108   
109    /** Filter for this detail level. */
110    // private String level;
111   
112    /** Should additional information be put into LaTeX output? E.g. QEDEQ reference names. */
113    private final boolean info;
114   
115    /** Current node id. */
116    private String id;
117   
118    /** Current node title. */
119    private String title;
120   
121    /** Sub context like "getIntroduction()". */
122    private String subContext = "";
123   
124    /** Maximum column number. If zero no line breaking is done automatically. */
125    private int maxColumns;
126   
127    /** Should warning messages be generated if LaTeX problems occur? */
128    private boolean addWarnings;
129   
130    /** Should only names and formulas be be printed? */
131    private final boolean brief;
132   
133    /** Alphabet for tagging. */
134    private static final String ALPHABET = "abcdefghijklmnopqrstuvwxyz";
135   
136    /** Printing data for a single formal proof line. */
137    private ProofLineData lineData = new ProofLineData();
138   
139    /** This is the maximal formula width. All proof line formulas that are bigger are wrapped. */
140    private int formulaWidth = 60;
141   
142    /** This is the maximal reason width. All proof line reasons that are bigger are wrapped. */
143    private int reasonWidth = 35;
144   
145    /** Tabulation string. */
146    private String tab = "";
147   
148    /**
149    * Constructor.
150    *
151    * @param plugin This plugin we work for.
152    * @param prop QEDEQ BO object.
153    * @param info Write reference info?
154    * @param maximumColumn Maximum column before automatic break.
155    * 0 means no automatic break.
156    * @param addWarnings Should warning messages be generated
157    * if LaTeX problems occur?
158    * @param brief Should only names and formulas be be printed?
159    */
 
160  17 toggle public Qedeq2UnicodeVisitor(final Plugin plugin, final KernelQedeqBo prop,
161    final boolean info, final int maximumColumn, final boolean addWarnings,
162    final boolean brief) {
163  17 super(plugin, prop);
164  17 this.info = info;
165  17 this.maxColumns = maximumColumn;
166  17 this.addWarnings = addWarnings;
167  17 this.brief = brief;
168    }
169   
170    /**
171    * Gives a UTF-8 representation of given QEDEQ module as InputStream.
172    *
173    * @param process We run in this process.
174    * @param printer Print herein.
175    * @param language Filter text to get and produce text in this language only.
176    * @param level Filter for this detail level. LATER 20100205 m31: not yet supported
177    * yet.
178    * @throws SourceFileExceptionList Major problem occurred.
179    * @throws IOException File IO failed.
180    */
 
181  17 toggle public void generateUtf8(final InternalServiceProcess process, final AbstractOutput printer,
182    final String language, final String level) throws SourceFileExceptionList, IOException {
183  17 setParameters(printer, language);
184  17 try {
185  17 traverse(process);
186    } finally {
187  17 getQedeqBo().addPluginErrorsAndWarnings((Plugin) getService(), getErrorList(), getWarningList());
188    }
189    }
190   
191    /**
192    * Set parameters.
193    *
194    * @param printer Print herein.
195    * @param language Choose this language.
196    */
 
197  17 toggle public void setParameters(final AbstractOutput printer,
198    final String language) {
199  17 this.printer = printer;
200  17 this.printer.setColumns(maxColumns);
201    // TODO 20110208 m31: perhaps we should have some config parameters for those percentage splittings
202  17 if (maxColumns <= 0) {
203  0 formulaWidth = 80;
204  0 reasonWidth = 50;
205  17 } else if (maxColumns <= 50) {
206  0 this.printer.setColumns(50);
207  0 formulaWidth = 21;
208  0 reasonWidth = 21;
209  17 } else if (maxColumns <= 100) {
210  17 formulaWidth = (maxColumns - 8) * 50 / 100;
211  17 reasonWidth = (maxColumns - 8) * 50 / 100;
212  0 } else if (maxColumns <= 120) {
213  0 reasonWidth = 46 + (maxColumns - 100) / 5;
214  0 formulaWidth = maxColumns - 8 - reasonWidth;
215    } else {
216  0 reasonWidth = 50 + (maxColumns - 120) / 10;
217  0 formulaWidth = maxColumns - 8 - reasonWidth;
218    }
219    // System.out.println("maxColums =" + this.printer.getColumns());
220    // System.out.println("formulaWidth =" + this.formulaWidth);
221    // System.out.println("reasonWidth =" + this.reasonWidth);
222  17 if (language == null) {
223  0 this.language = "en";
224    } else {
225  17 this.language = language;
226    }
227    // if (level == null) {
228    // this.level = "1";
229    // } else {
230    // this.level = level;
231    // }
232   
233  17 init();
234    }
235   
236    /**
237    * Reset counters and other variables. Should be executed before {@link #traverse()}.
238    */
 
239  17 toggle protected void init() {
240  17 id = null;
241  17 title = null;
242  17 subContext = "";
243    }
244   
 
245  17 toggle public final void visitEnter(final Qedeq qedeq) {
246  17 if (printer instanceof TextOutput) {
247  17 printer.println("================================================================================");
248  17 printer.println("UTF-8-file " + ((TextOutput) printer).getName());
249  17 printer.println("Generated from " + getQedeqBo().getModuleAddress());
250  17 printer.println("Generated at " + DateUtility.getTimestamp());
251  17 printer.println("================================================================================");
252  17 printer.println();
253  17 printer.println("If the characters of this document don't display correctly try opening this");
254  17 printer.println("document within a webbrowser and if necessary change the encoding to");
255  17 printer.println("Unicode (UTF-8)");
256  17 printer.println();
257  17 printer.println("Permission is granted to copy, distribute and/or modify this document");
258  17 printer.println("under the terms of the GNU Free Documentation License, Version 1.2");
259  17 printer.println("or any later version published by the Free Software Foundation;");
260  17 printer.println("with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts.");
261  17 printer.println();
262  17 printer.println();
263  17 printer.println();
264    }
265    }
266   
 
267  17 toggle public final void visitLeave(final Qedeq qedeq) {
268  17 printer.println();
269    }
270   
 
271  17 toggle public void visitEnter(final Header header) {
272  17 final LatexList tit = header.getTitle();
273  17 underlineBig(getLatexListEntry("getTitle()", tit));
274  17 printer.println();
275  17 final AuthorList authors = getQedeqBo().getQedeq().getHeader().getAuthorList();
276  17 final StringBuffer authorList = new StringBuffer();
277  34 for (int i = 0; i < authors.size(); i++) {
278  17 if (i > 0) {
279  0 authorList.append(" \n");
280  0 printer.println(", ");
281    }
282  17 final Author author = authors.get(i);
283  17 final String name = author.getName().getLatex().trim();
284  17 printer.print(name);
285  17 authorList.append(" " + name);
286  17 String email = author.getEmail();
287  17 if (email != null && email.trim().length() > 0) {
288  17 authorList.append(" <" + email + ">");
289    }
290    }
291  17 printer.println();
292  17 printer.println();
293  17 final String url = getQedeqBo().getUrl();
294  17 if (url != null && url.length() > 0) {
295  17 printer.println();
296  17 if ("de".equals(language)) {
297  8 printer.println("Die Quelle f\u00FCr dieses Dokument ist hier zu finden:");
298    } else {
299  9 if (!"en".equals(language)) {
300  0 printer.println("%%% TODO unknown language: " + language);
301    }
302  9 printer.println("The source for this document can be found here:");
303    }
304  17 printer.println();
305  17 printer.println(url);
306  17 printer.println();
307    }
308    {
309  17 printer.println();
310  17 if ("de".equals(language)) {
311  8 printer.println("Die vorliegende Publikation ist urheberrechtlich gesch\u00FCtzt.");
312    } else {
313  9 if (!"en".equals(language)) {
314  0 printer.println("%%% TODO unknown language: " + language);
315    }
316  9 printer.println("Copyright by the authors. All rights reserved.");
317    }
318    }
319  17 final String email = header.getEmail();
320  17 if (email != null && email.length() > 0) {
321  17 printer.println();
322  17 printer.println();
323  17 if ("de".equals(language)) {
324  8 printer.println("Bei Fragen, Anregungen oder Bitte um Aufnahme in die Liste der"
325    + " abh\u00E4ngigen Module schicken Sie bitte eine EMail an die Adresse "
326    + email);
327  8 printer.println();
328  8 printer.println();
329  8 printer.println("Die Autoren dieses Dokuments sind:");
330  8 printer.println();
331  8 printer.println(authorList);
332    } else {
333  9 if (!"en".equals(language)) {
334  0 printer.println("%%% TODO unknown language: " + language);
335    }
336  9 printer.println("If you have any questions, suggestions or want to add something"
337    + " to the list of modules that use this one, please send an email to the"
338    + " address " + email);
339  9 printer.println();
340  9 printer.println();
341  9 printer.println("The authors of this document are:");
342  9 printer.println(authorList);
343    }
344  17 printer.println();
345    }
346  17 printer.println();
347  17 printer.println();
348    }
349   
 
350  6 toggle public void visitEnter(final ImportList imports) throws ModuleDataException {
351    // this method call is a little bit odd but we have to print the imports
352    // also in the literature list and we don't want to have doubled code
353  6 printImports();
354    }
355   
356    /**
357    * Get URL for QEDEQ XML module.
358    *
359    * @param address Current module address.
360    * @param specification Find URL for this location list.
361    * @return URL or <code>""</code> if none (valid?) was found.
362    */
 
363  14 toggle private String getUrl(final ModuleAddress address, final Specification specification) {
364  14 final LocationList list = specification.getLocationList();
365  14 if (list == null || list.size() <= 0) {
366  0 return "";
367    }
368  14 try {
369  14 return address.getModulePaths(specification)[0].getUrl();
370    } catch (IOException e) {
371  0 return "";
372    }
373    }
374   
 
375  67 toggle public void visitEnter(final Chapter chapter) {
376    // check if we print only brief and test for non text subnodes
377  67 if (brief) {
378  0 boolean hasFormalContent = false;
379  0 do {
380  0 final SectionList sections = chapter.getSectionList();
381  0 if (sections == null) {
382  0 break;
383    }
384  0 for (int i = 0; i < sections.size() && !hasFormalContent; i++) {
385  0 final Section section = sections.get(i);
386  0 if (section == null) {
387  0 continue;
388    }
389  0 final SubsectionList subSections = section.getSubsectionList();
390  0 if (subSections == null) {
391  0 continue;
392    }
393  0 for (int j = 0; j < subSections.size(); j++) {
394  0 final SubsectionType subSection = subSections.get(j);
395  0 if (!(subSection instanceof Subsection)) {
396  0 hasFormalContent = true;
397  0 break;
398    }
399    }
400    }
401    } while (false);
402  0 if (!hasFormalContent) {
403  0 setBlocked(true);
404  0 return;
405    }
406    }
407  67 final QedeqNumbers numbers = getCurrentNumbers();
408  67 if (numbers.isChapterNumbering()) {
409  50 if ("de".equals(language)) {
410  22 printer.println("Kapitel " + numbers.getChapterNumber() + " ");
411    } else {
412  28 printer.println("Chapter " + numbers.getChapterNumber() + " ");
413    }
414  50 printer.println();
415  50 printer.println();
416    }
417  67 underlineBig(getLatexListEntry("getTitle()", chapter.getTitle()));
418  67 printer.println();
419  67 if (chapter.getIntroduction() != null && !brief) {
420  67 printer.append(getLatexListEntry("getIntroduction()", chapter.getIntroduction()));
421  67 printer.println();
422  67 printer.println();
423  67 printer.println();
424    }
425    }
426   
 
427  17 toggle public void visitLeave(final Header header) {
428  17 printer.println();
429  17 printer.println("___________________________________________________");
430  17 printer.println();
431  17 printer.println();
432    }
433   
 
434  67 toggle public void visitLeave(final Chapter chapter) {
435  67 if (!getBlocked()) {
436  67 printer.println();
437  67 printer.println("___________________________________________________");
438  67 printer.println();
439  67 printer.println();
440    }
441  67 setBlocked(false);
442    }
443   
 
444  131 toggle public void visitEnter(final Section section) {
445    // check if we print only brief and test for non text subnodes
446  131 if (brief) {
447  0 boolean hasFormalContent = false;
448  0 do {
449  0 final SubsectionList subSections = section.getSubsectionList();
450  0 if (subSections == null) {
451  0 break;
452    }
453  0 for (int j = 0; j < subSections.size(); j++) {
454  0 final SubsectionType subSection = subSections.get(j);
455  0 if (!(subSection instanceof Subsection)) {
456  0 hasFormalContent = true;
457  0 break;
458    }
459    }
460    } while (false);
461  0 if (!hasFormalContent) {
462  0 setBlocked(true);
463  0 return;
464    }
465    }
466  131 final QedeqNumbers numbers = getCurrentNumbers();
467  131 final StringBuffer buffer = new StringBuffer();
468  131 if (numbers.isChapterNumbering()) {
469  131 buffer.append(numbers.getChapterNumber());
470    }
471  131 if (numbers.isSectionNumbering()) {
472  131 if (buffer.length() > 0) {
473  131 buffer.append(".");
474    }
475  131 buffer.append(numbers.getSectionNumber());
476    }
477  131 if (buffer.length() > 0 && section.getTitle() != null) {
478  131 buffer.append(" ");
479    }
480  131 buffer.append(getLatexListEntry("getTitle()", section.getTitle()));
481  131 underline(buffer.toString());
482  131 printer.println();
483  131 if (section.getIntroduction() != null && !brief) {
484  131 printer.append(getLatexListEntry("getIntroduction()", section.getIntroduction()));
485  131 printer.println();
486  131 printer.println();
487  131 printer.println();
488    }
489    }
490   
 
491  131 toggle public void visitLeave(final Section section) {
492  131 if (!getBlocked()) {
493  131 printer.println();
494    }
495  131 setBlocked(false);
496    }
497   
 
498  48 toggle public void visitEnter(final Subsection subsection) {
499  48 if (brief) {
500  0 return;
501    }
502  48 final QedeqNumbers numbers = getCurrentNumbers();
503  48 final StringBuffer buffer = new StringBuffer();
504  48 if (numbers.isChapterNumbering()) {
505  48 buffer.append(numbers.getChapterNumber());
506    }
507  48 if (numbers.isSectionNumbering()) {
508  48 if (buffer.length() > 0) {
509  48 buffer.append(".");
510    }
511  48 buffer.append(numbers.getSectionNumber());
512    }
513  48 if (buffer.length() > 0) {
514  48 buffer.append(".");
515    }
516  48 buffer.append(numbers.getSubsectionNumber());
517  48 if (buffer.length() > 0 && subsection.getTitle() != null) {
518  30 buffer.append(" ");
519    }
520  48 if (subsection.getTitle() != null) {
521  30 printer.print(buffer.toString());
522  30 printer.print(getLatexListEntry("getTitle()", subsection.getTitle()));
523    }
524  48 if (subsection.getId() != null && info) {
525  2 printer.print(" [" + subsection.getId() + "]");
526    }
527  48 if (subsection.getTitle() != null) {
528  30 printer.println();
529  30 printer.println();
530    }
531  48 printer.append(getLatexListEntry("getLatex()", subsection.getLatex()));
532  48 printer.println();
533  48 printer.println();
534    }
535   
 
536  440 toggle public void visitEnter(final Node node) {
537  440 if (node.getPrecedingText() != null && !brief) {
538  232 printer.append(getLatexListEntry("getPrecedingText()", node.getPrecedingText()));
539  232 printer.println();
540  232 printer.println();
541    }
542  440 id = node.getId();
543  440 title = null;
544  440 if (node.getTitle() != null) {
545  236 title = getLatexListEntry("getTitle()", node.getTitle());
546    }
547    }
548   
 
549  440 toggle public void visitLeave(final Node node) {
550  440 if (node.getSucceedingText() != null && !brief) {
551  60 printer.append(getLatexListEntry("getSucceedingText()", node.getSucceedingText()));
552  60 printer.println();
553  60 printer.println();
554    }
555  440 printer.println();
556    }
557   
 
558  104 toggle public void visitEnter(final Axiom axiom) {
559  104 final QedeqNumbers numbers = getCurrentNumbers();
560  104 printer.print("\u2609 ");
561  104 printer.print("Axiom " + numbers.getAxiomNumber());
562  104 printer.print(" ");
563  104 if (title != null && title.length() > 0) {
564  104 printer.print(" (" + title + ")");
565    }
566  104 if (info) {
567  104 printer.print(" [" + id + "]");
568    }
569  104 printer.println();
570  104 printer.println();
571  104 printer.print(" ");
572  104 printFormula(axiom.getFormula().getElement());
573  104 printer.println();
574  104 if (axiom.getDescription() != null) {
575  0 printer.append(getLatexListEntry("getDescription()", axiom.getDescription()));
576  0 printer.println();
577  0 printer.println();
578    }
579    }
580   
 
581  206 toggle public void visitEnter(final Proposition proposition) {
582  206 final QedeqNumbers numbers = getCurrentNumbers();
583  206 printer.print("\u2609 ");
584  206 printer.print("Proposition " + numbers.getPropositionNumber());
585  206 printer.print(" ");
586  206 if (title != null && title.length() > 0) {
587  4 printer.print(" (" + title + ")");
588    }
589  206 if (info) {
590  206 printer.print(" [" + id + "]");
591    }
592  206 printer.println();
593  206 printer.println();
594  206 printTopFormula(proposition.getFormula().getElement(), id);
595  206 printer.println();
596  206 if (proposition.getDescription() != null) {
597  2 printer.append(getLatexListEntry("getDescription()", proposition.getDescription()));
598  2 printer.println();
599  2 printer.println();
600    }
601    }
602   
 
603  40 toggle public void visitEnter(final Proof proof) {
604  40 if (brief) {
605  0 setBlocked(true);
606  0 return;
607    }
608  40 if ("de".equals(language)) {
609  20 printer.println("Beweis:");
610    } else {
611  20 printer.println("Proof:");
612    }
613  40 printer.append(getLatexListEntry("getNonFormalProof()", proof.getNonFormalProof()));
614    }
615   
 
616  40 toggle public void visitLeave(final Proof proof) {
617  40 printer.println();
618  40 printer.println("q.e.d.");
619  40 printer.println();
620  40 setBlocked(false);
621    }
622   
 
623  82 toggle public void visitEnter(final FormalProof proof) {
624  82 if (brief) {
625  0 setBlocked(true);
626  0 return;
627    }
628  82 if ("de".equals(language)) {
629  41 printer.println("Beweis (formal):");
630    } else {
631  41 printer.println("Proof (formal):");
632    }
633    }
634   
 
635  82 toggle public void visitLeave(final FormalProof proof) {
636  82 if (!brief) {
637  82 printer.println("q.e.d.");
638  82 printer.println();
639    }
640  82 setBlocked(false);
641    }
642   
643   
 
644  836 toggle public void visitEnter(final FormalProofLine line) {
645  836 lineData.init();
646  836 if (line.getLabel() != null) {
647  836 lineData.setLineLabel(line.getLabel());
648    }
649  836 if (line.getReason() != null) {
650  836 setReason(line.getReason().toString());
651    }
652  836 setFormula(line.getFormula());
653    }
654   
 
655  836 toggle public void visitLeave(final FormalProofLine line) {
656  836 linePrintln();
657    }
658   
659    /**
660    * Print formula and reason.
661    */
 
662  1136 toggle private void linePrintln() {
663  1136 if (!lineData.containsData()) {
664  100 return;
665    }
666  1036 if (lineData.getLineLabel().length() > 0) {
667  1036 printer.print(StringUtility.alignRight("(" + lineData.getLineLabel() + ")", 5) + " ");
668    }
669  2194 for (int i = 0; i < lineData.lines(); i++) {
670  1158 printer.skipToColumn(6);
671  1158 printer.print(tab);
672  1158 if (i < lineData.getFormula().length) {
673  1158 printer.print(lineData.getFormula()[i]);
674    }
675  1158 if (i < lineData.getReason().length) {
676  1040 printer.skipToColumn(6 + 2 + formulaWidth);
677  1040 printer.print(lineData.getReason()[i]);
678    }
679  1158 printer.println();
680    }
681  1036 lineData.init();
682    }
683   
 
684  100 toggle public void visitEnter(final ConditionalProof r) throws ModuleDataException {
685  100 lineData.init();
686  100 printer.skipToColumn(6);
687  100 printer.print(tab);
688  100 printer.println("Conditional Proof");
689  100 tab = tab + " ";
690    }
691   
 
692  100 toggle public void visitLeave(final ConditionalProof proof) {
693  100 tab = StringUtility.substring(tab, 0, tab.length() - 2);
694    }
695   
 
696  100 toggle public void visitEnter(final Hypothesis hypothesis) {
697  100 lineData.init();
698  100 if (hypothesis.getLabel() != null) {
699  100 lineData.setLineLabel(hypothesis.getLabel());
700    }
701  100 setReason("Hypothesis");
702  100 setFormula(hypothesis.getFormula());
703    }
704   
 
705  100 toggle public void visitLeave(final Hypothesis hypothesis) {
706  100 linePrintln();
707    }
708   
 
709  100 toggle public void visitEnter(final Conclusion conclusion) {
710  100 tab = StringUtility.substring(tab, 0, tab.length() - 2);
711  100 lineData.init();
712  100 if (conclusion.getLabel() != null) {
713  100 lineData.setLineLabel(conclusion.getLabel());
714    }
715  100 setReason("Conclusion");
716  100 setFormula(conclusion.getFormula());
717  100 linePrintln();
718    }
719   
 
720  100 toggle public void visitLeave(final Conclusion conclusion) {
721  100 linePrintln();
722  100 tab = tab + " ";
723    }
724   
 
725  1872 toggle private void setReason(final String reasonString) {
726  1872 final List list = new ArrayList();
727  1872 int index = 0;
728  4172 while (index < reasonString.length()) {
729  2300 list.add(StringUtility.substring(reasonString, index, reasonWidth));
730  2300 index += reasonWidth;
731    }
732  1872 lineData.setReason((String[]) list.toArray(ArrayUtils.EMPTY_STRING_ARRAY));
733    }
734   
 
735  1036 toggle private void setFormula(final Formula f) {
736  1036 if (f != null && f.getElement() != null) {
737  1036 lineData.setFormula(getUtf8(f.getElement(),
738    formulaWidth - tab.length()));
739    }
740    }
741   
 
742  564 toggle private String getReference(final String reference) {
743  564 return getReference(reference, "getReference()");
744    }
745   
 
746  1108 toggle private String getReference(final String reference, final String subContext) {
747  1108 final String context = getCurrentContext().getLocationWithinModule();
748  1108 try {
749  1108 getCurrentContext().setLocationWithinModule(context + "." + subContext);
750  1108 return (getReferenceLink(reference, null, null));
751    } finally {
752  1108 getCurrentContext().setLocationWithinModule(context);
753    }
754    }
755   
 
756  272 toggle public void visitEnter(final ModusPonens r) throws ModuleDataException {
757  272 String buffer = r.getName();
758  272 boolean one = false;
759  272 if (r.getReference1() != null) {
760  272 buffer += " " + getReference(r.getReference1(), "getReference1()");
761  272 one = true;
762    }
763  272 if (r.getReference1() != null) {
764  272 if (one) {
765  272 buffer += ",";
766    }
767  272 buffer += " " + getReference(r.getReference2(), "getReference2()");
768    }
769  272 setReason(buffer);
770    }
771   
 
772  190 toggle public void visitEnter(final Add r) throws ModuleDataException {
773  190 String buffer = r.getName();
774  190 if (r.getReference() != null) {
775  190 buffer += " " + getReference(r.getReference());
776    }
777  190 setReason(buffer);
778    }
779   
 
780  16 toggle public void visitEnter(final Rename r) throws ModuleDataException {
781  16 String buffer = r.getName();
782  16 if (r.getOriginalSubjectVariable() != null) {
783  16 buffer += " " + getUtf8(r.getOriginalSubjectVariable());
784    }
785  16 if (r.getReplacementSubjectVariable() != null) {
786  16 buffer += " by " + getUtf8(r.getReplacementSubjectVariable());
787    }
788  16 if (r.getReference() != null) {
789  16 buffer += " in " + getReference(r.getReference());
790    }
791  16 setReason(buffer);
792    }
793   
 
794  10 toggle public void visitEnter(final SubstFree r) throws ModuleDataException {
795  10 String buffer = r.getName();
796  10 if (r.getSubjectVariable() != null) {
797  10 buffer += " " + getUtf8(r.getSubjectVariable());
798    }
799  10 if (r.getSubstituteTerm() != null) {
800  10 buffer += " by " + getUtf8(r.getSubstituteTerm());
801    }
802  10 if (r.getReference() != null) {
803  10 buffer += " in " + getReference(r.getReference());
804    }
805  10 setReason(buffer);
806    }
807   
 
808  2 toggle public void visitEnter(final SubstFunc r) throws ModuleDataException {
809  2 String buffer = r.getName();
810  2 if (r.getFunctionVariable() != null) {
811  2 buffer += " " + getUtf8(r.getFunctionVariable());
812    }
813  2 if (r.getSubstituteTerm() != null) {
814  2 buffer += " by " + getUtf8(r.getSubstituteTerm());
815    }
816  2 if (r.getReference() != null) {
817  2 buffer += " in " + getReference(r.getReference());
818    }
819  2 setReason(buffer);
820    }
821   
 
822  336 toggle public void visitEnter(final SubstPred r) throws ModuleDataException {
823  336 String buffer = r.getName();
824  336 if (r.getPredicateVariable() != null) {
825  336 buffer += " " + getUtf8(r.getPredicateVariable());
826    }
827  336 if (r.getSubstituteFormula() != null) {
828  336 buffer += " by " + getUtf8(r.getSubstituteFormula());
829    }
830  336 if (r.getReference() != null) {
831  336 buffer += " in " + getReference(r.getReference());
832    }
833  336 setReason(buffer);
834    }
835   
 
836  2 toggle public void visitEnter(final Existential r) throws ModuleDataException {
837  2 String buffer = r.getName();
838  2 if (r.getSubjectVariable() != null) {
839  2 buffer += " with " + getUtf8(r.getSubjectVariable());
840    }
841  2 if (r.getReference() != null) {
842  2 buffer += " in " + getReference(r.getReference());
843    }
844  2 setReason(buffer);
845    }
846   
 
847  8 toggle public void visitEnter(final Universal r) throws ModuleDataException {
848  8 String buffer = r.getName();
849  8 if (r.getSubjectVariable() != null) {
850  8 buffer += " with " + getQedeqBo().getElement2Utf8().getUtf8(
851    r.getSubjectVariable());
852    }
853  8 if (r.getReference() != null) {
854  8 buffer += " in " + getReference(r.getReference());
855    }
856  8 setReason(buffer);
857    }
858   
 
859  6 toggle public void visitEnter(final InitialPredicateDefinition definition) {
860  6 final QedeqNumbers numbers = getCurrentNumbers();
861  6 printer.print("\u2609 ");
862  6 final StringBuffer buffer = new StringBuffer();
863  6 if ("de".equals(language)) {
864  3 buffer.append("initiale ");
865    } else {
866  3 buffer.append("initial ");
867    }
868  6 buffer.append("Definition " + (numbers.getPredicateDefinitionNumber()
869    + numbers.getFunctionDefinitionNumber()));
870  6 printer.print(buffer.toString());
871  6 printer.print(" ");
872  6 if (title != null && title.length() > 0) {
873  6 printer.print(" (" + title + ")");
874    }
875  6 if (info) {
876  6 printer.print(" [" + id + "]");
877    }
878  6 printer.println();
879  6 printer.println();
880  6 printer.print(" ");
881  6 printer.println(getUtf8(definition.getPredCon()));
882  6 printer.println();
883  6 if (definition.getDescription() != null) {
884  0 printer.append(getLatexListEntry("getDescription()", definition.getDescription()));
885  0 printer.println();
886  0 printer.println();
887    }
888    }
889   
 
890  20 toggle public void visitEnter(final PredicateDefinition definition) {
891  20 final QedeqNumbers numbers = getCurrentNumbers();
892  20 printer.print("\u2609 ");
893  20 final StringBuffer buffer = new StringBuffer();
894  20 buffer.append("Definition " + (numbers.getPredicateDefinitionNumber()
895    + numbers.getFunctionDefinitionNumber()));
896  20 printer.print(buffer.toString());
897  20 printer.print(" ");
898  20 if (title != null && title.length() > 0) {
899  20 printer.print(" (" + title + ")");
900    }
901  20 if (info) {
902  20 printer.print(" [" + id + "]");
903    }
904  20 printer.println();
905  20 printer.println();
906  20 printer.print(" ");
907  20 printer.println(getUtf8(definition.getFormula().getElement()));
908  20 printer.println();
909  20 if (definition.getDescription() != null) {
910  0 printer.append(getLatexListEntry("getDescription()", definition.getDescription()));
911  0 printer.println();
912  0 printer.println();
913    }
914    }
915   
 
916  0 toggle public void visitEnter(final InitialFunctionDefinition definition) {
917  0 final QedeqNumbers numbers = getCurrentNumbers();
918  0 printer.print("\u2609 ");
919  0 final StringBuffer buffer = new StringBuffer();
920  0 if ("de".equals(language)) {
921  0 buffer.append("initiale ");
922    } else {
923  0 buffer.append("initial ");
924    }
925  0 buffer.append("Definition " + (numbers.getPredicateDefinitionNumber()
926    + numbers.getFunctionDefinitionNumber()));
927  0 printer.print(buffer.toString());
928  0 printer.print(" ");
929  0 if (title != null && title.length() > 0) {
930  0 printer.print(" (" + title + ")");
931    }
932  0 if (info) {
933  0 printer.print(" [" + id + "]");
934    }
935  0 printer.println();
936  0 printer.println();
937  0 printer.print(" ");
938  0 printer.println(getUtf8(definition.getFunCon()));
939  0 printer.println();
940  0 if (definition.getDescription() != null) {
941  0 printer.println(getLatexListEntry("getDescription()", definition.getDescription()));
942  0 printer.println();
943    }
944    }
945   
 
946  32 toggle public void visitEnter(final FunctionDefinition definition) {
947  32 final QedeqNumbers numbers = getCurrentNumbers();
948  32 printer.print("\u2609 ");
949  32 final StringBuffer buffer = new StringBuffer();
950  32 buffer.append("Definition " + (numbers.getPredicateDefinitionNumber()
951    + numbers.getFunctionDefinitionNumber()));
952  32 printer.print(buffer.toString());
953  32 printer.print(" ");
954  32 if (title != null && title.length() > 0) {
955  32 printer.print(" (" + title + ")");
956    }
957  32 if (info) {
958  32 printer.print(" [" + id + "]");
959    }
960  32 printer.println();
961  32 printer.println();
962  32 printer.print(" ");
963  32 printer.println(getUtf8(definition.getFormula().getElement()));
964  32 printer.println();
965  32 if (definition.getDescription() != null) {
966  0 printer.println(getLatexListEntry("getDescription()", definition.getDescription()));
967  0 printer.println();
968    }
969    }
970   
 
971  72 toggle public void visitEnter(final Rule rule) {
972  72 final QedeqNumbers numbers = getCurrentNumbers();
973  72 printer.print("\u2609 ");
974  72 if ("de".equals(language)) {
975  36 printer.print("Regel");
976    } else {
977  36 printer.print("Rule");
978    }
979  72 printer.print(" " + numbers.getRuleNumber());
980  72 printer.print(" ");
981  72 if (title != null && title.length() > 0) {
982  70 printer.print(" (" + title + ")");
983    }
984  72 if (info) {
985  72 printer.print(" [" + id + "]");
986    }
987  72 printer.println();
988  72 printer.println((rule.getName() != null ? " Name: " + rule.getName() : "")
989  72 + (rule.getVersion() != null ? " - Version: " + rule.getVersion() : ""));
990  72 printer.println();
991  72 if (rule.getDescription() != null) {
992  72 printer.append(getLatexListEntry("getDescription()", rule.getDescription()));
993  72 printer.println();
994  72 printer.println();
995    }
996    }
997   
 
998  4 toggle public void visitEnter(final LinkList linkList) {
999  4 if (linkList.size() <= 0) {
1000  0 return;
1001    }
1002  4 if ("de".equals(language)) {
1003  2 printer.println("Basierend auf: ");
1004    } else {
1005  2 if (!"en".equals(language)) {
1006  0 printer.println("%%% TODO unknown language: " + language);
1007    }
1008  2 printer.println("Based on: ");
1009    }
1010  10 for (int i = 0; i < linkList.size(); i++) {
1011  6 if (linkList.get(i) != null) {
1012  6 printer.print(" (" + linkList.get(i) + ")");
1013    }
1014  4 };
1015  4 printer.println();
1016    }
1017   
 
1018  2 toggle public void visitEnter(final ChangedRuleList list) {
1019  2 if (list.size() <= 0) {
1020  0 return;
1021    }
1022  2 printer.println();
1023  2 if ("de".equals(language)) {
1024  1 printer.println("Die folgenden Regeln m\u00FCssen erweitert werden.");
1025    } else {
1026  1 if (!"en".equals(language)) {
1027  0 printer.println("%%% TODO unknown language: " + language);
1028    }
1029  1 printer.println("The following rules have to be extended.");
1030    }
1031  2 printer.println();
1032    }
1033   
 
1034  16 toggle public void visitEnter(final ChangedRule rule) {
1035  16 printer.println((rule.getName() != null ? " Name: " + rule.getName() : "")
1036  16 + (rule.getVersion() != null ? " - Version: " + rule.getVersion() : ""));
1037  16 printer.println();
1038  16 if (rule.getDescription() != null) {
1039  16 printer.append(getLatexListEntry("getDescription()", rule.getDescription()));
1040  16 printer.println();
1041  16 printer.println();
1042    }
1043   
1044    }
1045   
 
1046  6 toggle public void visitEnter(final LiteratureItemList list) {
1047  6 printer.println();
1048  6 printer.println();
1049  6 if ("de".equals(language)) {
1050  3 underlineBig("Literaturverzeichnis");
1051    } else {
1052  3 underlineBig("Bibliography");
1053    }
1054  6 printImports();
1055    }
1056   
1057    /**
1058    * Print all imports if any.
1059    */
 
1060  12 toggle private void printImports() {
1061  12 final ImportList imports = getQedeqBo().getQedeq().getHeader().getImportList();
1062  12 if (imports != null && imports.size() > 0) {
1063  8 printer.println();
1064  8 printer.println();
1065  8 if ("de".equals(language)) {
1066  4 printer.println("Benutzte andere QEDEQ-Module:");
1067    } else {
1068  4 printer.println("Used other QEDEQ modules:");
1069    }
1070  8 printer.println();
1071  18 for (int i = 0; i < imports.size(); i++) {
1072  10 final Import imp = imports.get(i);
1073  10 printer.print("[" + imp.getLabel() + "] ");
1074  10 final Specification spec = imp.getSpecification();
1075  10 printer.print(spec.getName());
1076  10 if (spec.getLocationList() != null && spec.getLocationList().size() > 0
1077    && spec.getLocationList().get(0).getLocation().length() > 0) {
1078  10 printer.print(" ");
1079  10 printer.print(getUrl(getQedeqBo().getModuleAddress(), spec));
1080    }
1081  10 printer.println();
1082    }
1083  8 printer.println();
1084  8 printer.println();
1085    }
1086    }
1087   
 
1088  6 toggle public void visitLeave(final LiteratureItemList list) {
1089  6 final UsedByList usedby = getQedeqBo().getQedeq().getHeader().getUsedByList();
1090  6 if (usedby != null && usedby.size() > 0) {
1091  4 printer.println();
1092  4 printer.println();
1093  4 if ("de".equals(language)) {
1094  2 printer.println("QEDEQ-Module, welche dieses hier verwenden:");
1095    } else {
1096  2 printer.println("QEDEQ modules that use this one:");
1097    }
1098  8 for (int i = 0; i < usedby.size(); i++) {
1099  4 final Specification spec = usedby.get(i);
1100  4 printer.print(spec.getName());
1101  4 final String url = getUrl(getQedeqBo().getModuleAddress(), spec);
1102  4 if (url != null && url.length() > 0) {
1103  4 printer.print(" ");
1104  4 printer.print(url);
1105    }
1106  4 printer.println();
1107    }
1108  4 printer.println();
1109  4 printer.println();
1110    }
1111  6 printer.println();
1112    }
1113   
 
1114  28 toggle public void visitEnter(final LiteratureItem item) {
1115  28 printer.print("[" + item.getLabel() + "] ");
1116  28 printer.println(getLatexListEntry("getItem()", item.getItem()));
1117  28 printer.println();
1118    }
1119   
1120    /**
1121    * Print top level formula. If the formula has the form <code>AND(.., .., ..)</code> the
1122    * formula is broken down in several labeled lines.
1123    *
1124    * @param element Formula to print.
1125    * @param mainLabel Main formula label.
1126    */
 
1127  206 toggle private void printTopFormula(final Element element, final String mainLabel) {
1128  206 if (!element.isList() || !element.getList().getOperator().equals("AND")) {
1129  170 printer.print(" ");
1130  170 printFormula(element);
1131  170 return;
1132    }
1133  36 final ElementList list = element.getList();
1134  304 for (int i = 0; i < list.size(); i++) {
1135  268 String label = "";
1136  268 if (list.size() >= ALPHABET.length() * ALPHABET.length()) {
1137  0 label = "" + (i + 1);
1138    } else {
1139  268 if (list.size() > ALPHABET.length()) {
1140  80 final int div = (i / ALPHABET.length());
1141  80 label = "" + ALPHABET.charAt(div);
1142    }
1143  268 label += ALPHABET.charAt(i % ALPHABET.length());
1144    }
1145  268 printer.println(" (" + label + ") " + getUtf8(list.getElement(i)));
1146    }
1147    }
1148   
1149    /**
1150    * Print formula.
1151    *
1152    * @param element Formula to print.
1153    */
 
1154  274 toggle private void printFormula(final Element element) {
1155  274 printer.println(getUtf8(element));
1156    }
1157   
1158    /**
1159    * Filters correct entry out of LaTeX list. Filter criterion is for example the correct
1160    * language.
1161    *
1162    * @param method This method was called. Used to get the correct sub context.
1163    * Should not be null. If it is empty the <code>subContext</code>
1164    * is not changed.
1165    * @param list List of LaTeX texts.
1166    * @return Filtered text.
1167    */
 
1168  1177 toggle private String getLatexListEntry(final String method, final LatexList list) {
1169  1177 if (list == null) {
1170  0 return "";
1171    }
1172  1177 if (method.length() > 0) {
1173  1177 subContext = method;
1174    }
1175  1177 try {
1176  1729 for (int i = 0; i < list.size(); i++) {
1177  1617 if (language.equals(list.get(i).getLanguage())) {
1178  1065 if (method.length() > 0) {
1179  1065 subContext = method + ".get(" + i + ")";
1180    }
1181  1065 return getUtf8(list.get(i));
1182    }
1183    }
1184    // OK, we didn't found the language, so we take the default language
1185  112 final String def = getQedeqBo().getOriginalLanguage();
1186  122 for (int i = 0; i < list.size(); i++) {
1187  112 if (EqualsUtility.equals(def, list.get(i).getLanguage())) {
1188  102 if (method.length() > 0) {
1189  102 subContext = method + ".get(" + i + ")";
1190    }
1191  102 return "MISSING! OTHER: " + getUtf8(list.get(i));
1192    }
1193    }
1194    // OK, we didn't find wanted and default language, so we take the first non empty one
1195  11 for (int i = 0; i < list.size(); i++) {
1196  10 if (method.length() > 0) {
1197  10 subContext = method + ".get(" + i + ")";
1198    }
1199  10 if (null != list.get(i) && null != list.get(i).getLatex()
1200    && list.get(i).getLatex().trim().length() > 0) {
1201  9 return "MISSING! OTHER: " + getUtf8(list.get(i));
1202    }
1203    }
1204  1 return "MISSING!";
1205    } finally {
1206  1177 if (method.length() > 0) {
1207  1177 subContext = "";
1208    }
1209    }
1210    }
1211   
1212    /**
1213    * Get current module context. Uses sub context information.
1214    *
1215    * @param startDelta Skip position (relative to location start). Could be
1216    * <code>null</code>.
1217    * @param endDelta Mark until this column (relative to location start).
1218    * be <code>null</code>
1219    * @return Current module context.
1220    */
 
1221  1368 toggle private ModuleContext getCurrentContext(final SourcePosition startDelta,
1222    final SourcePosition endDelta) {
1223  1368 if (subContext.length() == 0) {
1224  1108 return super.getCurrentContext();
1225    }
1226  260 final ModuleContext c = new ModuleContext(super.getCurrentContext().getModuleLocation(),
1227    super.getCurrentContext().getLocationWithinModule() + "." + subContext,
1228    startDelta, endDelta);
1229  260 return c;
1230    }
1231   
1232    /**
1233    * Add warning.
1234    *
1235    * @param code Warning code.
1236    * @param msg Warning message.
1237    * @param startDelta Skip position (relative to location start). Could be
1238    * <code>null</code>.
1239    * @param endDelta Mark until this column (relative to location start). Could be
1240    * be <code>null</code>
1241    */
 
1242  30 toggle public void addWarning(final int code, final String msg, final SourcePosition startDelta,
1243    final SourcePosition endDelta) {
1244  30 Trace.param(CLASS, this, "addWarning", "msg", msg);
1245  30 if (addWarnings) {
1246  30 addWarning(new UnicodeException(code, msg, getCurrentContext(startDelta,
1247    endDelta)));
1248    }
1249    }
1250   
1251    /**
1252    * Add warning.
1253    *
1254    * @param code Warning code.
1255    * @param msg Warning message.
1256    */
 
1257  0 toggle public void addWarning(final int code, final String msg) {
1258  0 Trace.param(CLASS, this, "addWarning", "msg", msg);
1259  0 if (addWarnings) {
1260  0 addWarning(new UnicodeException(code, msg, getCurrentContext()));
1261    }
1262    }
1263   
1264    /**
1265    * Get Utf8 element presentation.
1266    *
1267    * @param element Get presentation of this element.
1268    * @param max Maximum column.
1269    * @return UTF-8 form of element.
1270    */
 
1271  1036 toggle protected String[] getUtf8(final Element element, final int max) {
1272  1036 return getQedeqBo().getElement2Utf8().getUtf8(element, max);
1273    }
1274   
1275   
1276    /**
1277    * Get Utf8 element presentation.
1278    *
1279    * @param element Get presentation of this element.
1280    * @return UTF-8 form of element.
1281    */
 
1282  1330 toggle protected String getUtf8(final Element element) {
1283  1330 return getUtf8(getQedeqBo().getElement2Latex().getLatex(element));
1284    }
1285   
1286    /**
1287    * Get UTF-8 String for LaTeX.
1288    *
1289    * @param latex LaTeX we got.
1290    * @return UTF-8 result string.
1291    */
 
1292  1176 toggle private String getUtf8(final Latex latex) {
1293  1176 if (latex == null || latex.getLatex() == null) {
1294  3 return "";
1295    }
1296  1173 return getUtf8(latex.getLatex());
1297    }
1298   
1299    /**
1300    * Transform LaTeX into UTF-8 String..
1301    *
1302    * @param latex LaTeX text.
1303    * @return String.
1304    */
 
1305  2503 toggle private String getUtf8(final String latex) {
1306  2503 if (latex == null) {
1307  0 return "";
1308    }
1309  2503 return Latex2UnicodeParser.transform(this, latex, maxColumns);
1310    }
1311   
1312    /**
1313    * Print text in one line and print another line with = to underline it.
1314    *
1315    * @param text Line to print.
1316    */
 
1317  90 toggle private void underlineBig(final String text) {
1318  90 printer.println(text);
1319  1963 for (int i = 0; i < text.length(); i++) {
1320  1873 printer.print("\u2550");
1321    }
1322  90 printer.println();
1323    }
1324   
1325    /**
1326    * Print text in one line and print another line with = to underline it.
1327    *
1328    * @param text Line to print.
1329    */
 
1330  131 toggle private void underline(final String text) {
1331  131 printer.println(text);
1332  3193 for (int i = 0; i < text.length(); i++) {
1333  3062 printer.print("\u2015");
1334    }
1335  131 printer.println();
1336    }
1337   
 
1338  1338 toggle public String getReferenceLink(final String reference, final SourcePosition start,
1339    final SourcePosition end) {
1340  1338 final Reference ref = getReference(reference, getCurrentContext(start, end), addWarnings,
1341    false);
1342   
1343  1338 if (ref.isNodeLocalReference() && ref.isSubReference()) {
1344  0 return "(" + ref.getSubLabel() + ")";
1345    }
1346   
1347  1338 if (ref.isNodeLocalReference() && ref.isProofLineReference()) {
1348  918 return "(" + ref.getProofLineLabel() + ")";
1349    }
1350   
1351  420 if (!ref.isExternal()) {
1352  350 return getNodeDisplay(ref.getNodeLabel(), ref.getNode())
1353  350 + (ref.isSubReference() ? " (" + ref.getSubLabel() + ")" : "")
1354  350 + (ref.isProofLineReference() ? " (" + ref.getProofLineLabel() + ")" : "");
1355    }
1356   
1357    // do we have an external module reference without node?
1358  70 if (ref.isExternalModuleReference()) {
1359  2 return "[" + ref.getExternalQedeqLabel() + "]";
1360    }
1361   
1362  68 return getNodeDisplay(ref.getNodeLabel(), ref.getNode())
1363  68 + (ref.isSubReference() ? " (" + ref.getSubLabel() + ")" : "")
1364  68 + (ref.isProofLineReference() ? " (" + ref.getProofLineLabel() + ")" : "")
1365  68 + (ref.isExternal() ? " [" + ref.getExternalQedeqLabel() + "]" : "");
1366    }
1367   
 
1368  418 toggle private String getNodeDisplay(final String label, final KernelNodeBo kNode) {
1369  418 return getNodeDisplay(label, kNode, language);
1370    }
1371   
1372    }
 
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 .