Clover coverage report - QedeqKernelSe Coverage Report
Coverage timestamp: So Sep 2 2007 02:40:58 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 1.080   Methods: 37
NCLOC: 838   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
Qedeq2Latex.java 69,3% 83,1% 100% 79,8%
coverage coverage
 1    /* $Id: Qedeq2Latex.java,v 1.47 2007/05/10 00:37:53 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.module.ModuleDataException;
 55    import org.qedeq.kernel.bo.module.QedeqBo;
 56    import org.qedeq.kernel.bo.visitor.AbstractModuleVisitor;
 57    import org.qedeq.kernel.bo.visitor.QedeqNotNullTransverser;
 58    import org.qedeq.kernel.dto.module.PredicateDefinitionVo;
 59    import org.qedeq.kernel.trace.Trace;
 60    import org.qedeq.kernel.utility.IoUtility;
 61    import org.qedeq.kernel.utility.ReplaceUtility;
 62    import org.qedeq.kernel.utility.TextOutput;
 63   
 64   
 65    /**
 66    * Transfer a QEDEQ module into a LaTeX file.
 67    * <p>
 68    * <b>TODO mime 20070131: This is just a quick written generator. No parsing or validation
 69    * of inline LaTeX text is done. No references to other QEDEQ modules are resolved. This class just
 70    * generates some LaTeX output to be able to get a visual impression of a QEDEQ module.</b>
 71    * <p>
 72    * This generator operates operates against the interface declaration of a QEDEQ module.
 73    * A business object is not yet required.
 74    *
 75    *
 76    * @version $Revision: 1.47 $
 77    * @author Michael Meyling
 78    */
 79    public final class Qedeq2Latex extends AbstractModuleVisitor {
 80   
 81    /** Transverse QEDEQ module with this transverser. */
 82    private final QedeqNotNullTransverser transverser;
 83   
 84    /** Output goes here. */
 85    private final TextOutput printer;
 86   
 87    /** QEDEQ BO object to work on. */
 88    private final QedeqBo qedeq;
 89   
 90    /** Filter text to get and produce text in this language. */
 91    private final String language;
 92   
 93    /** Filter for this detail level. TODO mime 20050205: not used yet. */
 94    private final String level;
 95   
 96    /** Maps identifiers to {@link PredicateDefinition}s. */
 97    private final Map predicateDefinitions = new HashMap();
 98   
 99    /** Maps identifiers to {@link FunctionDefinition}s. */
 100    private final Map functionDefinitions = new HashMap();
 101   
 102    /** Current chapter number, starting with 0. */
 103    private int chapterNumber;
 104   
 105    /** Current section number, starting with 0. */
 106    private int sectionNumber;
 107   
 108    /** Current node id. */
 109    private String id;
 110   
 111    /** Current node title. */
 112    private String title;
 113   
 114    /** Alphabet for tagging. */
 115    private static final String ALPHABET = "abcdefghijklmnopqrstuvwxyz";
 116   
 117    /**
 118    * Constructor.
 119    *
 120    * @param qedeq QEDEQ BO object.
 121    * @param globalContext Module location information.
 122    * @param printer Print herein.
 123    * @param language Filter text to get and produce text in this language only.
 124    * @param level Filter for this detail level. TODO mime 20050205: not supported yet.
 125    */
 126  22 private Qedeq2Latex(final QedeqBo qedeq, final String globalContext,
 127    final TextOutput printer, final String language, final String level) {
 128  22 this.qedeq = qedeq;
 129  22 this.transverser = new QedeqNotNullTransverser(globalContext, this);
 130  22 this.printer = printer;
 131  22 if (language == null) {
 132  3 this.language = "en";
 133    } else {
 134  19 this.language = language;
 135    }
 136  22 if (level == null) {
 137  9 this.level = "1";
 138    } else {
 139  13 this.level = level;
 140    }
 141  22 final PredicateDefinitionVo equal = new PredicateDefinitionVo();
 142    // LATER mime 20050224: quick hack to have the logical identity operator
 143  22 equal.setArgumentNumber("2");
 144  22 equal.setName("equal");
 145  22 equal.setLatexPattern("#1 \\ = \\ #2");
 146  22 predicateDefinitions.put("equal_2", equal);
 147    // TODO mime 20060822: quick hack to get the negation of the logical identity operator
 148  22 final PredicateDefinitionVo notEqual = new PredicateDefinitionVo();
 149  22 notEqual.setArgumentNumber("2");
 150  22 notEqual.setName("notEqual");
 151  22 notEqual.setLatexPattern("#1 \\ \\neq \\ #2");
 152  22 predicateDefinitions.put("notEqual_2", notEqual);
 153    }
 154   
 155    /**
 156    * Prints a XML representation of given QEDEQ module into a given output stream.
 157    *
 158    * @param globalContext Module location information.
 159    * @param qedeq Basic QEDEQ module object.
 160    * @param printer Print herein.
 161    * @param language Filter text to get and produce text in this language only.
 162    * @param level Filter for this detail level. TODO mime 20050205: not supported yet.
 163    * @throws ModuleDataException Major problem occurred.
 164    * @throws IOException
 165    */
 166  22 public static void print(final String globalContext, final QedeqBo qedeq,
 167    final TextOutput printer, final String language, final String level)
 168    throws ModuleDataException, IOException {
 169  22 final Qedeq2Latex converter = new Qedeq2Latex(qedeq, globalContext, printer,
 170    language, level);
 171  22 converter.printLatex();
 172    }
 173   
 174    /**
 175    * Prints a XML file into a given output stream.
 176    * Constructs a {@link QedeqBo} first.
 177    *
 178    * @throws IOException Writing failed.
 179    * @throws ModuleDataException Exception during transversion.
 180    */
 181  22 private final void printLatex() throws IOException, ModuleDataException {
 182  22 transverser.accept(qedeq);
 183  22 printer.flush();
 184  22 if (printer.checkError()) {
 185  0 throw printer.getError();
 186    }
 187    }
 188   
 189  22 public final void visitEnter(final Qedeq qedeq) {
 190  22 printer.println("% -*- TeX:" + language.toUpperCase() + " -*-");
 191  22 printer.println("%%% ====================================================================");
 192  22 printer.println("%%% @LaTeX-file " + printer.getName());
 193  22 printer.println("%%% Generated at " + getTimestamp());
 194  22 printer.println("%%% ====================================================================");
 195  22 printer.println();
 196  22 printer.println(
 197    "%%% Permission is granted to copy, distribute and/or modify this document");
 198  22 printer.println("%%% under the terms of the GNU Free Documentation License, Version 1.2");
 199  22 printer.println("%%% or any later version published by the Free Software Foundation;");
 200  22 printer.println(
 201    "%%% with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts.");
 202  22 printer.println();
 203  22 printer.println("\\documentclass[a4paper,german,10pt,twoside]{book}");
 204  22 if ("de".equals(language)) {
 205  8 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  22 printer.println("\\usepackage{makeidx}");
 213  22 printer.println("\\usepackage{amsmath,amsthm,amssymb}");
 214  22 printer.println("\\usepackage{color}");
 215  22 printer.println("\\usepackage[bookmarks,bookmarksnumbered,bookmarksopen,");
 216  22 printer.println(" colorlinks,linkcolor=webgreen,pagebackref]{hyperref}");
 217  22 printer.println("\\definecolor{webgreen}{rgb}{0,.5,0}");
 218  22 printer.println("\\usepackage{graphicx}");
 219  22 printer.println("\\usepackage{xr}");
 220  22 printer.println("\\usepackage{epsfig,longtable}");
 221  22 printer.println("\\usepackage{tabularx}");
 222  22 printer.println();
 223  22 if ("de".equals(language)) {
 224  8 printer.println("\\newtheorem{thm}{Theorem}[chapter]");
 225  8 printer.println("\\newtheorem{cor}[thm]{Korollar}");
 226  8 printer.println("\\newtheorem{lem}[thm]{Lemma}");
 227  8 printer.println("\\newtheorem{prop}[thm]{Proposition}");
 228  8 printer.println("\\newtheorem{ax}{Axiom}");
 229  8 printer.println("\\newtheorem{rul}{Regel}");
 230  8 printer.println();
 231  8 printer.println("\\theoremstyle{definition}");
 232  8 printer.println("\\newtheorem{defn}[thm]{Definition}");
 233  8 printer.println("\\newtheorem{idefn}[thm]{Initiale Definition}");
 234  8 printer.println();
 235  8 printer.println("\\theoremstyle{remark}");
 236  8 printer.println("\\newtheorem{rem}[thm]{Bemerkung}");
 237  8 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  22 printer.println();
 258  22 printer.println("\\addtolength{\\textheight}{7\\baselineskip}");
 259  22 printer.println("\\addtolength{\\topmargin}{-5\\baselineskip}");
 260  22 printer.println();
 261  22 printer.println("\\setlength{\\parindent}{0pt}");
 262  22 printer.println();
 263  22 printer.println("\\frenchspacing \\sloppy");
 264  22 printer.println();
 265  22 printer.println("\\makeindex");
 266  22 printer.println();
 267  22 printer.println();
 268    }
 269   
 270  22 public final void visitLeave(final Qedeq qedeq) {
 271  22 printer.println("\\backmatter");
 272  22 printer.println();
 273  22 printer.println("\\addcontentsline{toc}{chapter}{\\indexname} \\printindex");
 274  22 printer.println();
 275  22 printer.println("\\end{document}");
 276  22 printer.println();
 277    }
 278   
 279  22 public void visitEnter(final Header header) {
 280  22 final LatexList title = header.getTitle();
 281  22 printer.print("\\title{");
 282  22 printer.print(getLatexListEntry(title));
 283  22 printer.println("}");
 284  22 printer.println("\\author{");
 285  22 final AuthorList authors = qedeq.getHeader().getAuthorList();
 286  22 for (int i = 0; i < authors.size(); i++) {
 287  22 if (i > 0) {
 288  0 printer.println(", ");
 289    }
 290  22 final Author author = authors.get(i);
 291  22 printer.print(author.getName().getLatex());
 292    // TODO mime 20070206 if (author.getEmail() != null)
 293    }
 294  22 printer.println();
 295  22 printer.println("}");
 296  22 printer.println();
 297  22 printer.println("\\begin{document}");
 298  22 printer.println();
 299  22 printer.println("\\maketitle");
 300  22 printer.println();
 301  22 printer.println("\\setlength{\\parskip}{5pt plus 2pt minus 1pt}");
 302  22 printer.println("\\mbox{}");
 303  22 printer.println("\\vfill");
 304  22 printer.println();
 305  22 final String url = getUrl(header.getSpecification());
 306  22 if (url != null && url.length() > 0) {
 307  22 printer.println("\\par");
 308  22 if ("de".equals(language)) {
 309  8 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  22 printer.println("\\par");
 317  22 printer.println("\\url{" + getUrl(header.getSpecification()) + "}");
 318  22 printer.println();
 319    }
 320    {
 321  22 printer.println("\\par");
 322  22 if ("de".equals(language)) {
 323  8 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  22 final String email = header.getEmail();
 332  22 if (email != null && email.length() > 0) {
 333  22 final String emailUrl = "\\url{mailto:" + email + "}";
 334  22 printer.println("\\par");
 335  22 if ("de".equals(language)) {
 336  8 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  22 printer.println();
 348    }
 349  22 printer.println("\\setlength{\\parskip}{0pt}");
 350  22 printer.println("\\tableofcontents");
 351  22 printer.println();
 352  22 printer.println("\\setlength{\\parskip}{5pt plus 2pt minus 1pt}");
 353  22 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  2 return "";
 367    }
 368  44 String location = list.get(0).getLocation();
 369  44 if (!location.endsWith("/")) {
 370  44 location += "/";
 371    }
 372  44 location += specification.getName();
 373  44 location += ".xml";
 374  44 return location;
 375    }
 376   
 377  66 public void visitEnter(final Chapter chapter) {
 378  66 printer.print("\\chapter");
 379  66 if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) {
 380  16 printer.print("*");
 381    }
 382  66 printer.print("{");
 383  66 printer.print(getLatexListEntry(chapter.getTitle()));
 384  66 final String label = "chapter" + chapterNumber;
 385  66 printer.println("} \\label{" + label + "} \\hypertarget{" + label + "}{}");
 386  66 if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) {
 387  16 printer.println("\\addcontentsline{toc}{chapter}{"
 388    + getLatexListEntry(chapter.getTitle()) + "}");
 389    }
 390  66 printer.println();
 391  66 if (chapter.getIntroduction() != null) {
 392  63 printer.println(getLatexListEntry(chapter.getIntroduction()));
 393  63 printer.println();
 394    }
 395    }
 396   
 397  66 public void visitLeave(final Chapter chapter) {
 398  66 printer.println("%% end of chapter " + getLatexListEntry(chapter.getTitle()));
 399  66 printer.println();
 400  66 chapterNumber++; // increase global chapter number
 401  66 sectionNumber = 0; // reset section number
 402    }
 403   
 404  44 public void visitLeave(final SectionList list) {
 405  44 printer.println();
 406    }
 407   
 408  106 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  106 printer.print("\\section{");
 415  106 printer.print(getLatexListEntry(section.getTitle()));
 416  106 final String label = "chapter" + chapterNumber + "_section" + sectionNumber;
 417  106 printer.println("} \\label{" + label + "} \\hypertarget{" + label + "}{}");
 418  106 printer.println(getLatexListEntry(section.getIntroduction()));
 419  106 printer.println();
 420    }
 421   
 422  106 public void visitLeave(final Section section) {
 423  106 sectionNumber++; // increase global section number
 424    }
 425   
 426  46 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=\