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