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