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: 925   Methods: 22
NCLOC: 699   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
Qedeq2LatexOld.java 0% 0% 0% 0%
coverage
 1    /* $Id: Qedeq2LatexOld.java,v 1.1 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.io.OutputStream;
 22    import java.io.PrintStream;
 23    import java.text.SimpleDateFormat;
 24    import java.util.Date;
 25    import java.util.HashMap;
 26    import java.util.Map;
 27   
 28    import org.qedeq.kernel.base.list.Element;
 29    import org.qedeq.kernel.base.list.ElementList;
 30    import org.qedeq.kernel.base.module.Author;
 31    import org.qedeq.kernel.base.module.AuthorList;
 32    import org.qedeq.kernel.base.module.Axiom;
 33    import org.qedeq.kernel.base.module.Chapter;
 34    import org.qedeq.kernel.base.module.ChapterList;
 35    import org.qedeq.kernel.base.module.FunctionDefinition;
 36    import org.qedeq.kernel.base.module.Latex;
 37    import org.qedeq.kernel.base.module.LatexList;
 38    import org.qedeq.kernel.base.module.LiteratureItem;
 39    import org.qedeq.kernel.base.module.LiteratureItemList;
 40    import org.qedeq.kernel.base.module.Node;
 41    import org.qedeq.kernel.base.module.NodeType;
 42    import org.qedeq.kernel.base.module.PredicateDefinition;
 43    import org.qedeq.kernel.base.module.Proposition;
 44    import org.qedeq.kernel.base.module.Qedeq;
 45    import org.qedeq.kernel.base.module.Rule;
 46    import org.qedeq.kernel.base.module.Section;
 47    import org.qedeq.kernel.base.module.SectionList;
 48    import org.qedeq.kernel.base.module.Subsection;
 49    import org.qedeq.kernel.base.module.SubsectionList;
 50    import org.qedeq.kernel.base.module.SubsectionType;
 51    import org.qedeq.kernel.base.module.VariableList;
 52    import org.qedeq.kernel.bo.control.QedeqBoFactory;
 53    import org.qedeq.kernel.bo.module.ModuleDataException;
 54    import org.qedeq.kernel.dto.module.PredicateDefinitionVo;
 55    import org.qedeq.kernel.log.Trace;
 56    import org.qedeq.kernel.utility.IoUtility;
 57    import org.qedeq.kernel.utility.ReplaceUtility;
 58   
 59   
 60    /**
 61    * FIXME mime 20070205: remove before release. This file is replaced by Qedeq2Latex.
 62    *
 63    * Transfer a QEDEQ module into a LaTeX file.
 64    * <p>
 65    * <b>mime 20050205: This is just a quick hacked generator. No parsing or validation
 66    * of inline LaTeX text is done. No reference is resolved. This class just
 67    * generates some LaTeX to get some visual impression of a QEDEQ module
 68    * in an early development stage.</b>
 69    * <p>
 70    * This generator operates operates against the interface declaration of a QEDEQ module.
 71    * No business object is required.
 72    *
 73    * @version $Revision: 1.1 $
 74    * @author Michael Meyling
 75    */
 76    public final class Qedeq2LatexOld {
 77   
 78    /** Alphabet for tagging. */
 79    private static final String ALPHABET = "abcdefghijklmnopqrstuvwxyz";
 80   
 81    /** Output goes here. */
 82    private PrintStream printer;
 83   
 84    /** Qedeq module to transfer into LaTeX form. */
 85    private Qedeq qedeq;
 86   
 87    /** Filter text to get and produce text in this language. */
 88    private String language;
 89   
 90    /** Filter for this detail level. */
 91    private Object level;
 92   
 93    /** Maps identifiers to {@link PredicateDefinition}s. */
 94    private Map definitions = new HashMap();
 95   
 96    /**
 97    * Constructor.
 98    *
 99    * @param context Context within this module is created.
 100    * @param qedeq Work with this qedeq module.
 101    * @throws ModuleDataException
 102    */
 103  0 public Qedeq2LatexOld(final String context, final Qedeq qedeq) throws ModuleDataException {
 104    // although we work against the interfaces we create an BO just for testing purposes
 105  0 this.qedeq = QedeqBoFactory.createQedeq(context, qedeq);
 106  0 final PredicateDefinitionVo equal = new PredicateDefinitionVo();
 107    // LATER mime 20050224: quick hack to have the logical identity operator
 108  0 equal.setArgumentNumber("2");
 109  0 equal.setName("equal");
 110  0 equal.setLatexPattern("#1 \\ = \\ #2");
 111  0 definitions.put("equal_2", equal);
 112    // LATER mime 20060822: quick hack to get the negation of the logical identity operator
 113  0 final PredicateDefinitionVo notEqual = new PredicateDefinitionVo();
 114  0 notEqual.setArgumentNumber("2");
 115  0 notEqual.setName("notEqual");
 116  0 notEqual.setLatexPattern("#1 \\ \\neq \\ #2");
 117  0 definitions.put("notEqual_2", notEqual);
 118    }
 119   
 120    /**
 121    * Prints a LaTeX file into a given output stream.
 122    *
 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    * @param outputStream Write output herein.
 126    * @throws IOException
 127    */
 128  0 public final synchronized void printLatex(final String language, final String level,
 129    final OutputStream outputStream) throws IOException {
 130  0 if (language == null) {
 131  0 this.language = "en";
 132    } else {
 133  0 this.language = language;
 134    }
 135  0 if (level == null) {
 136  0 this.level = "1";
 137    } else {
 138  0 this.level = level;
 139    }
 140  0 this.printer = new PrintStream(outputStream);
 141  0 printLatexHeader();
 142  0 printQedeqHeader();
 143  0 printQedeqChapters();
 144  0 printQedeqBibliography();
 145  0 printLatexTrailer();
 146  0 if (printer.checkError()) {
 147  0 throw new IOException("TODO mime: better use another OutputStream");
 148    }
 149    }
 150   
 151    /**
 152    * Prints the header.
 153    */
 154  0 private void printQedeqHeader() {
 155  0 final LatexList title = qedeq.getHeader().getTitle();
 156  0 printer.print("\\title{");
 157  0 printer.print(getLatexListEntry(title));
 158  0 printer.println("}");
 159  0 printer.println("\\author{");
 160  0 final AuthorList authors = qedeq.getHeader().getAuthorList();
 161  0 for (int i = 0; i < authors.size(); i++) {
 162  0 if (i > 0) {
 163  0 printer.println(", ");
 164    }
 165  0 final Author author = authors.get(i);
 166  0 printer.print(author.getName().getLatex());
 167    }
 168  0 printer.println();
 169  0 printer.println("}");
 170  0 printer.println();
 171  0 printer.println("\\begin{document}");
 172  0 printer.println();
 173  0 printer.println("\\maketitle");
 174  0 printer.println();
 175  0 printer.println("\\setlength{\\parskip}{0pt}");
 176  0 printer.println("\\tableofcontents");
 177  0 printer.println("\\setlength{\\parskip}{5pt plus 2pt minus 1pt}");
 178  0 printer.println();
 179    }
 180   
 181    /**
 182    * Print all chapters.
 183    */
 184  0 private void printQedeqChapters() {
 185  0 final ChapterList chapters = qedeq.getChapterList();
 186  0 for (int i = 0; i < chapters.size(); i++) {
 187  0 final Chapter chapter = chapters.get(i);
 188  0 printer.print("\\chapter");
 189  0 if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) {
 190  0 printer.print("*");
 191    }
 192  0 printer.print("{");
 193  0 printer.print(getLatexListEntry(chapter.getTitle()));
 194  0 final String label = "chapter" + i;
 195  0 printer.println("} \\label{" + label + "} \\hypertarget{" + label + "}{}");
 196  0 if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) {
 197  0 printer.println("\\addcontentsline{toc}{chapter}{"
 198    + getLatexListEntry(chapter.getTitle()) + "}");
 199    }
 200  0 printer.println();
 201  0 if (chapter.getIntroduction() != null) {
 202  0 printer.println(getLatexListEntry(chapter.getIntroduction()));
 203  0 printer.println();
 204    }
 205  0 final SectionList sections = chapter.getSectionList();
 206  0 if (sections != null) {
 207  0 printSections(i, sections);
 208  0 printer.println();
 209    }
 210  0 printer.println("%% end of chapter " + getLatexListEntry(chapter.getTitle()));
 211  0 printer.println();
 212    }
 213    }
 214   
 215    /**
 216    * Print bibliography (if any).
 217    */
 218  0 private void printQedeqBibliography() {
 219  0 final LiteratureItemList items = qedeq.getLiteratureItemList();
 220  0 if (items == null) {
 221  0 return;
 222    }
 223  0 printer.println("\\begin{thebibliography}{99}");
 224  0 for (int i = 0; i < items.size(); i++) {
 225  0 final LiteratureItem item = items.get(i);
 226  0 printer.print("\\bibitem{" + item.getLabel() + "} ");
 227  0 printer.println(getLatexListEntry(item.getItem()));
 228  0 printer.println();
 229    }
 230  0 printer.println("\\end{thebibliography}");
 231    // TODO mime 20060926: remove language dependency
 232  0 if ("de".equals(language)) {
 233  0 printer.println("\\addcontentsline{toc}{chapter}{Literaturverzeichnis}");
 234    } else {
 235  0 printer.println("\\addcontentsline{toc}{chapter}{Bibliography}");
 236    }
 237   
 238    }
 239   
 240    /**
 241    * Print all given sections.
 242    *
 243    * @param chapter Chapter number.
 244    * @param sections List of sections.
 245    */
 246  0 private void printSections(final int chapter, final SectionList sections) {
 247  0 if (sections == null) {
 248  0 return;
 249    }
 250  0 for (int i = 0; i < sections.size(); i++) {
 251  0 final Section section = sections.get(i);
 252  0 printer.print("\\section{");
 253  0 printer.print(getLatexListEntry(section.getTitle()));
 254  0 final String label = "chapter" + chapter + "_section" + i;
 255  0 printer.println("} \\label{" + label + "} \\hypertarget{" + label + "}{}");
 256  0 printer.println(getLatexListEntry(section.getIntroduction()));
 257  0 printer.println();
 258  0 printSubsections(section.getSubsectionList());
 259    }
 260    }
 261   
 262    /**
 263    * Print all given subsections.
 264    *
 265    * @param nodes List of subsections.
 266    */
 267  0 private void printSubsections(final SubsectionList nodes) {
 268  0 if (nodes == null) {
 269  0 return;
 270    }
 271  0 for (int i = 0; i < nodes.size(); i++) {
 272  0 final SubsectionType subsectionType = nodes.get(i);
 273  0 if (subsectionType instanceof Node) {
 274  0 final Node node = (Node) subsectionType;
 275  0 printer.println("\\par");
 276  0 printer.println(getLatexListEntry(node.getPrecedingText()));
 277  0 printer.println();
 278  0 final String id = node.getId();
 279  0 final NodeType type = node.getNodeType();
 280  0 String title = null;
 281  0 if (node.getTitle() != null) {
 282  0 title = getLatexListEntry(node.getTitle());
 283    }
 284  0 if (type instanceof Axiom) {
 285  0 printAxiom((Axiom) type, title, id);
 286  0 } else if (type instanceof PredicateDefinition) {
 287  0 printPredicateDefinition((PredicateDefinition) type, title, id);
 288  0 } else if (type instanceof FunctionDefinition) {
 289  0 printFunctionDefinition((FunctionDefinition) type, title, id);
 290  0 } else if (type instanceof Proposition) {
 291  0 printProposition((Proposition) type, title, id);
 292  0 } else if (type instanceof Rule) {
 293  0 printRule((Rule) type, title, id);
 294    } else {
 295  0 throw new RuntimeException((type != null ? "unknown type: "
 296    + type.getClass().getName() : "node type empty"));
 297    }
 298  0 printer.println();
 299  0 printer.println(getLatexListEntry(node.getSucceedingText()));
 300    } else {
 301  0 final Subsection subsection = (Subsection) subsectionType;
 302  0 if (subsection.getTitle() != null) {
 303  0 printer.print("\\subsection{");
 304  0 printer.println(getLatexListEntry(subsection.getTitle()));
 305  0 printer.println("}");
 306    }
 307  0 printer.println(getLatexListEntry(subsection.getLatex()));
 308    }
 309  0 printer.println();
 310  0 printer.println();
 311    }
 312    }
 313   
 314    /**
 315    * Print axiom.
 316    *
 317    * @param axiom Print this.
 318    * @param title Extra name.
 319    * @param id Label for marking this axiom.
 320    */
 321  0 private void printAxiom(final Axiom axiom, final String title, final String id) {
 322  0 printer.println("\\begin{ax}" + (title != null ? "[" + title + "]" : ""));
 323  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 324  0 printFormula(axiom.getFormula().getElement());
 325  0 printer.println(getLatexListEntry(axiom.getDescription()));
 326  0 printer.println("\\end{ax}");
 327    }
 328   
 329    /**
 330    * Print top level formula. If the formula has the form <code>AND(.., .., ..)</code> the
 331    * formula is broken down in several labeled lines.
 332    *
 333    * @param element Formula to print.
 334    * @param mainLabel Main formula label.
 335    */
 336  0 private void printTopFormula(final Element element, final String mainLabel) {
 337  0 if (!element.isList() || !element.getList().getOperator().equals("AND")) {
 338  0 printFormula(element);
 339  0 return;
 340    }
 341  0 final ElementList list = element.getList();
 342  0 printer.println("\\mbox{}");
 343  0 printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{0.9\\linewidth}l}}");
 344  0 for (int i = 0; i < list.size(); i++) {
 345  0 final String label = (i < ALPHABET.length() ? "" + ALPHABET .charAt(i) : "" + i);
 346  0 printer.println("\\centering $" + getLatex(list.getElement(i)) + "$"
 347    + " & \\label{" + mainLabel + ":" + label + "} \\hypertarget{" + mainLabel + ":"
 348    + label + "}{} \\mbox{\\emph{(" + label + ")}} "
 349  0 + (i + 1 < list.size() ? "\\\\" : ""));
 350    }
 351  0 printer.println("\\end{longtable}");
 352    }
 353   
 354    /**
 355    * Print formula.
 356    *
 357    * @param element Formula to print.
 358    */
 359  0 private void printFormula(final Element element) {
 360  0 printer.println("\\mbox{}");
 361  0 printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{\\linewidth}}}");
 362  0 printer.println("\\centering $" + getLatex(element) + "$");
 363  0 printer.println("\\end{longtable}");
 364    }
 365   
 366    /**
 367    * Print predicate definition.
 368    *
 369    * @param definition Print this.
 370    * @param title Extra name.
 371    * @param id Label for marking this definition.
 372    */
 373  0 private void printPredicateDefinition(final PredicateDefinition definition, final String title,
 374    final String id) {
 375  0 final StringBuffer define = new StringBuffer("$$" + definition.getLatexPattern());
 376  0 final VariableList list = definition.getVariableList();
 377  0 if (list != null) {
 378  0 for (int i = list.size() - 1; i >= 0; i--) {
 379  0 Trace.trace(this, "printPredicateDefinition", "replacing!");
 380  0 ReplaceUtility.replace(define, "#" + (i + 1), getLatex(list.get(i)));
 381    }
 382    }
 383  0 if (definition.getFormula() != null) {
 384  0 printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : ""));
 385  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 386  0 define.append("\\ :\\leftrightarrow \\ ");
 387  0 define.append(getLatex(definition.getFormula().getElement()));
 388    } else {
 389  0 printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : ""));
 390  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 391    }
 392  0 define.append("$$");
 393  0 definitions.put(definition.getName() + "_" + definition.getArgumentNumber(), definition);
 394  0 Trace.param(this, "printPredicateDefinition", "define", define);
 395  0 printer.println(define);
 396  0 printer.println(getLatexListEntry(definition.getDescription()));
 397  0 if (definition.getFormula() != null) {
 398  0 printer.println("\\end{defn}");
 399    } else {
 400  0 printer.println("\\end{idefn}");
 401    }
 402    }
 403   
 404    /**
 405    * Print function definition.
 406    *
 407    * @param definition Print this.
 408    * @param title Extra name.
 409    * @param id Label for marking this definition.
 410    */
 411  0 private void printFunctionDefinition(final FunctionDefinition definition, final String title,
 412    final String id) {
 413  0 final StringBuffer define = new StringBuffer("$$" + definition.getLatexPattern());
 414  0 final VariableList list = definition.getVariableList();
 415  0 if (list != null) {
 416  0 for (int i = list.size() - 1; i >= 0; i--) {
 417  0 Trace.trace(this, "printFunctionDefinition", "replacing!");
 418  0 ReplaceUtility.replace(define, "#" + (i + 1), getLatex(list.get(i)));
 419    }
 420    }
 421  0 if (definition.getTerm() != null) {
 422  0 printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : ""));
 423  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 424  0 define.append("\\ := \\ ");
 425  0 define.append(getLatex(definition.getTerm().getElement()));
 426    } else {
 427  0 printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : ""));
 428  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 429    }
 430  0 define.append("$$");
 431  0 definitions.put(definition.getName() + "_" + definition.getArgumentNumber(), definition);
 432  0 Trace.param(this, "printFunctionDefinition", "define", define);
 433