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?