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  0 printer.println(define);
 434  0 printer.println(getLatexListEntry(definition.getDescription()));
 435  0 if (definition.getTerm() != null) {
 436  0 printer.println("\\end{defn}");
 437    } else {
 438  0 printer.println("\\end{idefn}");
 439    }
 440    }
 441   
 442    /**
 443    * Print proposition.
 444    *
 445    * @param proposition Print this.
 446    * @param title Extra name.
 447    * @param id Label for marking this proposition.
 448    */
 449  0 private void printProposition(final Proposition proposition, final String title,
 450    final String id) {
 451  0 printer.println("\\begin{prop}" + (title != null ? "[" + title + "]" : ""));
 452  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 453  0 printTopFormula(proposition.getFormula().getElement(), id);
 454  0 printer.println(getLatexListEntry(proposition.getDescription()));
 455  0 printer.println("\\end{prop}");
 456  0 if (proposition.getProofList() != null) {
 457  0 for (int i = 0; i < proposition.getProofList().size(); i++) {
 458  0 printer.println("\\begin{proof}");
 459  0 printer.println(getLatexListEntry(proposition.getProofList().get(i)
 460    .getNonFormalProof()));
 461  0 printer.println("\\end{proof}");
 462    }
 463    }
 464    }
 465   
 466    /**
 467    * Print rule declaration.
 468    *
 469    * @param rule Print this.
 470    * @param title Extra name.
 471    * @param id Label for marking this proposition.
 472    */
 473  0 private void printRule(final Rule rule, final String title,
 474    final String id) {
 475  0 printer.println("\\begin{rul}" + (title != null ? "[" + title + "]" : ""));
 476  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 477  0 printer.println(getLatexListEntry(rule.getDescription()));
 478  0 printer.println("\\end{rul}");
 479   
 480    // TODO mime 20051210: are these informations equivalent to a formal proof?
 481    /*
 482    if (null != rule.getLinkList()) {
 483    printer.println("\\begin{proof}");
 484    printer.println("Rule name: " + rule.getName());
 485    printer.println();
 486    printer.println();
 487    for (int i = 0; i < rule.getLinkList().size(); i++) {
 488    printer.println(rule.getLinkList().get(i));
 489    }
 490    printer.println("\\end{proof}");
 491    }
 492    */
 493  0 if (rule.getProofList() != null) {
 494  0 for (int i = 0; i < rule.getProofList().size(); i++) {
 495  0 printer.println("\\begin{proof}");
 496  0 printer.println(getLatexListEntry(rule.getProofList().get(i)
 497    .getNonFormalProof()));
 498  0 printer.println("\\end{proof}");
 499    }
 500    }
 501    }
 502   
 503    /**
 504    * Get LaTeX element presentation.
 505    *
 506    * @param element Print this element.
 507    * @return LaTeX form of element.
 508    */
 509  0 private String getLatex(final Element element) {
 510  0 return getLatex(element, true);
 511    }
 512   
 513    /**
 514    * Get LaTeX element presentation.
 515    *
 516    * @param element Print this element.
 517    * @param first First level?
 518    * @return LaTeX form of element.
 519    */
 520  0 private String getLatex(final Element element, final boolean first) {
 521  0 final StringBuffer buffer = new StringBuffer();
 522  0 if (element.isAtom()) {
 523  0 return element.getAtom().getString();
 524    }
 525  0 final ElementList list = element.getList();
 526  0 if (list.getOperator().equals("PREDCON")) {
 527  0 final String identifier = list.getElement(0).getAtom().getString() + "_"
 528    + (list.size() - 1);
 529    // TODO mime 20060922: is only working for definition name + argument number
 530    // if argument length is dynamic this dosen't work
 531  0 if (definitions.containsKey(identifier)) {
 532  0 final PredicateDefinition definition = (PredicateDefinition)
 533    definitions.get(identifier);
 534  0 final StringBuffer define = new StringBuffer(definition.getLatexPattern());
 535  0 for (int i = list.size() - 1; i >= 1; i--) {
 536  0 ReplaceUtility.replace(define, "#" + i, getLatex(list.getElement(i), false));
 537    }
 538  0 buffer.append(define);
 539    } else {
 540  0 buffer.append(identifier);
 541  0 buffer.append("(");
 542  0 for (int i = 1; i < list.size(); i++) {
 543  0 buffer.append(getLatex(list.getElement(i), false));
 544  0 if (i + 1 < list.size()) {
 545  0 buffer.append(", ");
 546    }
 547    }
 548  0 buffer.append(")");
 549    }
 550  0 } else if (list.getOperator().equals("PREDVAR")) {
 551  0 final String identifier = list.getElement(0).getAtom().getString();
 552  0 buffer.append(identifier);
 553  0 if (list.size() > 1) {
 554  0 buffer.append("(");
 555  0 for (int i = 1; i < list.size(); i++) {
 556  0 buffer.append(getLatex(list.getElement(i), false));
 557  0 if (i + 1 < list.size()) {
 558  0 buffer.append(", ");
 559    }
 560    }
 561  0 buffer.append(")");
 562    }
 563  0 } else if (list.getOperator().equals("FUNCON")) {
 564  0 final String identifier = list.getElement(0).getAtom().getString() + "_"
 565    + (list.size() - 1);
 566    // TODO mime 20060922: is only working for definition name + argument number
 567    // if argument length is dynamic this dosen't work
 568  0 if (definitions.containsKey(identifier)) {
 569  0 final FunctionDefinition definition = (FunctionDefinition)
 570    definitions.get(identifier);
 571  0 final StringBuffer define = new StringBuffer(definition.getLatexPattern());
 572  0 for (int i = list.size() - 1; i >= 1; i--) {
 573  0 ReplaceUtility.replace(define, "#" + i, getLatex(list.getElement(i), false));
 574    }
 575  0 buffer.append(define);
 576    } else {
 577  0 buffer.append(identifier);
 578  0 buffer.append("(");
 579  0 for (int i = 1; i < list.size(); i++) {
 580  0 buffer.append(getLatex(list.getElement(i), false));
 581  0 if (i + 1 < list.size()) {
 582  0 buffer.append(", ");
 583    }
 584    }
 585  0 buffer.append(")");
 586    }
 587  0 } else if (list.getOperator().equals("FUNVAR")) {
 588  0 final String identifier = list.getElement(0).getAtom().getString();
 589  0 buffer.append(identifier);
 590  0 if (list.size() > 1) {
 591  0 buffer.append("(");
 592  0 for (int i = 1; i < list.size(); i++) {
 593  0 buffer.append(getLatex(list.getElement(i), false));
 594  0 if (i + 1 < list.size()) {
 595  0 buffer.append(", ");
 596    }
 597    }
 598  0 buffer.append(")");
 599    }
 600  0 } else if (list.getOperator().equals("VAR")) {
 601  0 final String text = list.getElement(0).getAtom().getString();
 602    // interpret variable identifier as number
 603  0 try {
 604  0 final int index = Integer.parseInt(text);
 605  0 final String newText = "" + index;
 606  0 if (!text.equals(newText) || newText.startsWith("-")) {
 607  0 throw new NumberFormatException("This is no allowed number: " + text);
 608    }
 609  0 switch (index) {
 610  0 case 1:
 611  0 return "x";
 612  0 case 2:
 613  0 return "y";
 614  0 case 3:
 615  0 return "z";
 616  0 case 4:
 617  0 return "u";
 618  0 case 5:
 619  0 return "v";
 620  0 case 6:
 621  0 return "w";
 622  0 default:
 623  0 return "x_" + (index - 6);
 624    }
 625    } catch (NumberFormatException e) {
 626    // variable identifier is no number, just take it as it is
 627  0 return text;
 628    }
 629  0 } else if (list.getOperator().equals("AND") || list.getOperator().equals("OR")
 630    || list.getOperator().equals("EQUI") || list.getOperator().equals("IMPL")) {
 631  0 final String infix;
 632  0 if (list.getOperator().equals("AND")) {
 633  0 infix = "\\ \\land \\ ";
 634  0 } else if (list.getOperator().equals("OR")) {
 635  0 infix = "\\ \\lor \\ ";
 636  0 } else if (list.getOperator().equals("EQUI")) {
 637  0 infix = "\\ \\leftrightarrow \\ ";
 638    } else {
 639  0 infix = "\\ \\rightarrow \\ ";
 640    }
 641  0 if (!first) {
 642  0 buffer.append("(");
 643    }
 644  0 for (int i = 0; i < list.size(); i++) {
 645  0 buffer.append(getLatex(list.getElement(i), false));
 646  0 if (i + 1 < list.size()) {
 647  0 buffer.append(infix);
 648    }
 649    }
 650  0 if (!first) {
 651  0 buffer.append(")");
 652    }
 653  0 } else if (list.getOperator().equals("FORALL") || list.getOperator().equals("EXISTS")
 654    || list.getOperator().equals("EXISTSU")) {
 655  0 final String prefix;
 656  0 if (list.getOperator().equals("FORALL")) {
 657  0 prefix = "\\forall ";
 658  0 } else if (list.getOperator().equals("EXISTS")) {
 659  0 prefix = "\\exists ";
 660    } else {
 661  0 prefix = "\\exists! ";
 662    }
 663  0 buffer.append(prefix);
 664  0 for (int i = 0; i < list.size(); i++) {
 665  0 if (i != 0 || (i == 0 && list.size() <= 2)) {
 666  0 buffer.append(getLatex(list.getElement(i), false));
 667    }
 668  0 if (i + 1 < list.size()) {
 669  0 buffer.append("\\ ");
 670    }
 671  0 if (list.size() > 2 && i == 1) {
 672  0 buffer.append("\\ ");
 673    }
 674    }
 675  0 } else if (list.getOperator().equals("NOT")) {
 676  0 final String prefix = "\\neg ";
 677  0 buffer.append(prefix);
 678  0 for (int i = 0; i < list.size(); i++) {
 679  0 buffer.append(getLatex(list.getElement(i), false));
 680    }
 681  0 } else if (list.getOperator().equals("CLASS")) {
 682  0 final String prefix = "\\{ ";
 683  0 buffer.append(prefix);
 684  0 for (int i = 0; i < list.size(); i++) {
 685  0 buffer.append(getLatex(list.getElement(i), false));
 686  0 if (i + 1 < list.size()) {
 687  0 buffer.append(" \\ | \\ ");
 688    }
 689    }
 690  0 buffer.append(" \\} ");
 691  0 } else if (list.getOperator().equals("CLASSLIST")) {
 692  0 final String prefix = "\\{ ";
 693  0 buffer.append(prefix);
 694  0 for (int i = 0; i < list.size(); i++) {
 695  0 buffer.append(getLatex(list.getElement(i), false));
 696  0 if (i + 1 < list.size()) {
 697  0 buffer.append(", \\ ");
 698    }
 699    }
 700  0 buffer.append(" \\} ");
 701  0 } else if (list.getOperator().equals("QUANTOR_INTERSECTION")) {
 702  0 final String prefix = "\\bigcap";
 703  0 buffer.append(prefix);
 704  0 if (0 < list.size()) {
 705  0 buffer.append("{").append(getLatex(list.getElement(0), false)).append("}");
 706    }
 707  0 for (int i = 1; i < list.size(); i++) {
 708  0 buffer.append(getLatex(list.getElement(i), false));
 709  0 if (i + 1 < list.size()) {
 710  0 buffer.append(" \\ \\ ");
 711    }
 712    }
 713  0 buffer.append(" \\} ");
 714  0 } else if (list.getOperator().equals("QUANTOR_UNION")) {
 715  0 final String prefix = "\\bigcup";
 716  0 buffer.append(prefix);
 717  0 if (0 < list.size()) {
 718  0 buffer.append("{").append(getLatex(list.getElement(0), false)).append("}");
 719    }
 720  0 for (int i = 1; i < list.size(); i++) {
 721  0 buffer.append(getLatex(list.getElement(i), false));
 722  0 if (i + 1 < list.size()) {
 723  0 buffer.append(" \\ \\ ");
 724    }
 725    }
 726  0 buffer.append(" \\} ");
 727    } else {
 728  0 buffer.append(list.getOperator());
 729  0 buffer.append("(");
 730  0 for (int i = 0; i < list.size(); i++) {
 731  0 buffer.append(getLatex(list.getElement(i), false));
 732  0 if (i + 1 < list.size()) {
 733  0 buffer.append(", ");
 734    }
 735    }
 736  0 buffer.append(")");
 737    }
 738  0 return buffer.toString();
 739    }
 740   
 741    /**
 742    * Print LaTeX lines for the file head.
 743    */
 744  0 private void printLatexHeader() {
 745  0 printer.println("% -*- TeX:" + language.toUpperCase() + " -*-");
 746  0 printer.println("%%% ====================================================================");
 747  0 printer.println("%%% @LaTeX-file " + getFileName());
 748  0 printer.println("%%% Generated at " + getTimestamp());
 749  0 printer.println("%%% ====================================================================");
 750  0 printer.println();
 751  0 printer.println(
 752    "%%% Permission is granted to copy, distribute and/or modify this document");
 753  0 printer.println("%%% under the terms of the GNU Free Documentation License, Version 1.2");
 754  0 printer.println("%%% or any later version published by the Free Software Foundation;");
 755  0 printer.println(
 756    "%%% with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts.");
 757  0 printer.println();
 758  0 printer.println("\\documentclass[a4paper,german,10pt,twoside]{book}");
 759  0 if ("de".equals(language)) {
 760  0 printer.println("\\usepackage[german]{babel}");
 761  0 } else if ("en".equals(language)) {
 762  0 printer.println("\\usepackage[english]{babel}");
 763    } else {
 764  0 printer.println("%%% TODO unknown language: " + language);
 765  0 printer.println("%%% TODO using default language");
 766  0 printer.println("\\usepackage[english]{babel}");
 767    }
 768  0 printer.println("\\usepackage{makeidx}");
 769  0 printer.println("\\usepackage{amsmath,amsthm,amssymb}");
 770  0 printer.println("\\usepackage{color}");
 771  0 printer.println("\\usepackage[bookmarks,bookmarksnumbered,bookmarksopen,");
 772  0 printer.println(" colorlinks,linkcolor=webgreen,pagebackref]{hyperref}");
 773  0 printer.println("\\definecolor{webgreen}{rgb}{0,.5,0}");
 774  0 printer.println("\\usepackage{graphicx}");
 775  0 printer.println("\\usepackage{xr}");
 776  0 printer.println("\\usepackage{epsfig,longtable}");
 777  0 printer.println("\\usepackage{tabularx}");
 778  0 printer.println();
 779  0 if ("de".equals(language)) {
 780  0 printer.println("\\newtheorem{thm}{Theorem}[chapter]");
 781  0 printer.println("\\newtheorem{cor}[thm]{Korollar}");
 782  0 printer.println("\\newtheorem{lem}[thm]{Lemma}");
 783  0 printer.println("\\newtheorem{prop}[thm]{Proposition}");
 784  0 printer.println("\\newtheorem{ax}{Axiom}");
 785  0 printer.println("\\newtheorem{rul}{Regel}");
 786  0 printer.println();
 787  0 printer.println("\\theoremstyle{definition}");
 788  0 printer.println("\\newtheorem{defn}[thm]{Definition}");
 789  0 printer.println("\\newtheorem{idefn}[thm]{Initiale Definition}");
 790  0 printer.println();
 791  0 printer.println("\\theoremstyle{remark}");
 792  0 printer.println("\\newtheorem{rem}[thm]{Bemerkung}");
 793  0 printer.println("\\newtheorem*{notation}{Notation}");
 794  0 } else if ("en".equals(language)) {
 795  0 printer.println("\\newtheorem{thm}{Theorem}[chapter]");
 796  0 printer.println("\\newtheorem{cor}[thm]{Corollary}");
 797  0 printer.println("\\newtheorem{lem}[thm]{Lemma}");
 798  0 printer.println("\\newtheorem{prop}[thm]{Proposition}");
 799  0 printer.println("\\newtheorem{ax}{Axiom}");
 800  0 printer.println("\\newtheorem{rul}{Rule}");
 801  0 printer.println();
 802  0 printer.println("\\theoremstyle{definition}");
 803  0 printer.println("\\newtheorem{defn}[thm]{Definition}");
 804  0 printer.println("\\newtheorem{idefn}[thm]{Initial Definition}");
 805  0 printer.println();
 806  0 printer.println("\\theoremstyle{remark}");
 807  0 printer.println("\\newtheorem{rem}[thm]{Remark}");
 808  0 printer.println("\\newtheorem*{notation}{Notation}");
 809    } else {
 810  0 printer.println("%%% TODO unknown language: " + language);
 811  0 printer.println("%%% TODO using default language");
 812  0 printer.println("\\newtheorem{thm}{Theorem}[chapter]");
 813  0 printer.println("\\newtheorem{cor}[thm]{Corollary}");
 814  0 printer.println("\\newtheorem{lem}[thm]{Lemma}");
 815  0 printer.println("\\newtheorem{prop}[thm]{Proposition}");
 816  0 printer.println("\\newtheorem{ax}{Axiom}");
 817  0 printer.println();
 818  0 printer.println("\\theoremstyle{definition}");
 819  0 printer.println("\\newtheorem{defn}[thm]{Definition}");
 820  0 printer.println("\\newtheorem{idefn}[thm]{Initial Definition}");
 821  0 printer.println();
 822  0 printer.println("\\theoremstyle{remark}");
 823  0 printer.println("\\newtheorem{rem}[thm]{Remark}");
 824  0 printer.println("\\newtheorem*{notation}{Notation}");
 825    }
 826  0 printer.println();
 827  0 printer.println("\\addtolength{\\textheight}{7\\baselineskip}");
 828  0 printer.println("\\addtolength{\\topmargin}{-5\\baselineskip}");
 829  0 printer.println();
 830  0 printer.println("\\setlength{\\parindent}{0pt}");
 831  0 printer.println();
 832  0 printer.println("\\frenchspacing \\sloppy");
 833  0 printer.println();
 834  0 printer.println("\\makeindex");
 835  0 printer.println();
 836  0 printer.println();
 837    }
 838   
 839    /**
 840    * Print LaTeX trailer.
 841    */
 842  0 private void printLatexTrailer() {
 843  0 printer.println("\\backmatter");
 844  0 printer.println();
 845  0 printer.println("\\addcontentsline{toc}{chapter}{\\indexname} \\printindex");
 846  0 printer.println();
 847  0 printer.println("\\end{document}");
 848  0 printer.println();
 849    }
 850   
 851    /**
 852    * Get regular name for the LaTeX file.
 853    *
 854    * @return File name.
 855    */
 856  0 private String getFileName() {
 857    // FIXME mime 20050805: add language, validate with currently used file name e.g.
 858    // qedeq_basic_concept_en.tex
 859  0 return qedeq.getHeader().getSpecification().getName() + "_"
 860    + qedeq.getHeader().getSpecification().getRuleVersion() + ".tex";
 861    }
 862   
 863    /**
 864    * Get timestamp.
 865    *
 866    * @return Current timestamp.
 867    */
 868  0 private String getTimestamp() {
 869  0 final SimpleDateFormat formatter = new SimpleDateFormat("yyyy-MM-dd' 'HH:mm:ss,SSS");
 870  0 return formatter.format(new Date());
 871    }
 872   
 873    /**
 874    * Filters correct entry out of LaTeX list. Filter criterion is for example the correct
 875    * language.
 876    * TODO mime 20050205: filter level too?
 877    *
 878    * @param list List of LaTeX texts.
 879    * @return Filtered text.
 880    */
 881  0 private String getLatexListEntry(final LatexList list) {
 882  0 if (list == null) {
 883  0 return "";
 884    }
 885  0 for (int i = 0; i < list.size(); i++) {
 886  0 if (language.equals(list.get(i).getLanguage())) {
 887  0 return getLatex(list.get(i));
 888    }
 889    }
 890    // assume entry with missing language as default
 891  0 for (int i = 0; i < list.size(); i++) {
 892  0 if (list.get(i).getLanguage() == null) {
 893  0 return getLatex(list.get(i));
 894    }
 895    }
 896  0 for (int i = 0; i < list.size(); i++) { // LATER mime 20050222: evaluate default?
 897  0 return "MISSING! OTHER: " + getLatex(list.get(i));
 898    }
 899  0 return "MISSING!";
 900    }
 901   
 902    /**
 903    * Get really LaTeX. Does some simple character replacements for umlauts.
 904    * TODO mime 20050205: filter more than German umlauts
 905    *
 906    * @param latex Unescaped text.
 907    * @return Really LaTeX.
 908    */
 909  0 private String getLatex(final Latex latex) {
 910  0 if (latex.getLatex() == null) {
 911  0 return "";
 912    }
 913  0 final StringBuffer buffer = new StringBuffer(latex.getLatex());
 914  0 IoUtility.deleteLineLeadingWhitespace(buffer);
 915  0 ReplaceUtility.replace(buffer, "\u00fc", "{\\\"u}");
 916  0 ReplaceUtility.replace(buffer, "\u00f6", "{\\\"o}");
 917  0 ReplaceUtility.replace(buffer, "\u00e4", "{\\\"a}");
 918  0 ReplaceUtility.replace(buffer, "\u00dc", "{\\\"U}");
 919  0 ReplaceUtility.replace(buffer, "\u00d6", "{\\\"O}");
 920  0 ReplaceUtility.replace(buffer, "\u00c4", "{\\\"A}");
 921  0 ReplaceUtility.replace(buffer, "\u00df", "{\\ss}");
 922  0 return buffer.toString();
 923    }
 924   
 925    }
 
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.