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