Clover coverage report - QedeqKernelSe Coverage Report
Coverage timestamp: Do Jan 11 2007 09:03:50 CET
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 919   Methods: 22
NCLOC: 695   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
Qedeq2Latex.java 67,3% 77,4% 100% 74,9%
coverage coverage
 1    /* $Id: Qedeq2Latex.java,v 1.41 2006/10/20 20:23:08 m31 Exp $
 2    *
 3    * This file is part of the project "Hilbert II" - http://www.qedeq.org
 4    *
 5    * Copyright 2000-2006, 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    * Transfer a qedeq module into a LaTeX file.
 62    * <p>
 63    * <b>TODO mime 20050205: This is just a quick hacked generator. No parsing or validation
 64    * of inline LaTeX text is done. No reference is resolved. This class just
 65    * generates some LaTeX to get some visual impression of a QEDEQ module
 66    * in an early development stage.</b>
 67    * <p>
 68    * This generator operates operates against the interface declaration of a QEDEQ module.
 69    * No business object is required.
 70    *
 71    * @version $Revision: 1.41 $
 72    * @author Michael Meyling
 73    */
 74    public final class Qedeq2Latex {
 75   
 76    /** Alphabet for tagging. */
 77    private static final String ALPHABET = "abcdefghijklmnopqrstuvwxyz";
 78   
 79    /** Output goes here. */
 80    private PrintStream printer;
 81   
 82    /** Qedeq module to transfer into LaTeX form. */
 83    private Qedeq qedeq;
 84   
 85    /** Filter text to get and produce text in this language. */
 86    private String language;
 87   
 88    /** Filter for this detail level. TODO mime 20050205: not used yet. */
 89    private Object level;
 90   
 91    /** Maps identifiers to {@link PredicateDefinition}s. */ // FIXME mime 20070102: also for Function Definitions!!!
 92    private Map definitions = new HashMap();
 93   
 94    /**
 95    * Constructor.
 96    *
 97    * @param context Context within this module is created.
 98    * @param qedeq Work with this qedeq module.
 99    * @throws ModuleDataException
 100    */
 101  11 public Qedeq2Latex(final String context, final Qedeq qedeq) throws ModuleDataException {
 102    // although we work against the interfaces we create an BO just for testing purposes
 103  11 this.qedeq = QedeqBoFactory.createQedeq(context, qedeq);
 104  10 final PredicateDefinitionVo equal = new PredicateDefinitionVo();
 105    // TODO mime 20050224: quick hack to have the logical identity operator
 106  10 equal.setArgumentNumber("2");
 107  10 equal.setName("equal");
 108  10 equal.setLatexPattern("#1 \\ = \\ #2");
 109  10 definitions.put("equal_2", equal);
 110    // TODO mime 20060822: quick hack to get the negation of the logical identity operator
 111  10 final PredicateDefinitionVo notEqual = new PredicateDefinitionVo();
 112  10 notEqual.setArgumentNumber("2");
 113  10 notEqual.setName("notEqual");
 114  10 notEqual.setLatexPattern("#1 \\ \\neq \\ #2");
 115  10 definitions.put("notEqual_2", notEqual);
 116    }
 117   
 118    /**
 119    * Prints a LaTeX file into a given output stream.
 120    *
 121    * @param language Filter text to get and produce text in this language only.
 122    * @param level Filter for this detail level. TODO mime 20050205: not supported yet.
 123    * @param outputStream Write output herein.
 124    * @throws IOException
 125    */
 126  10 public final synchronized void printLatex(final String language, final String level,
 127    final OutputStream outputStream) throws IOException {
 128  10 if (language == null) {
 129  0 this.language = "en";
 130    } else {
 131  10 this.language = language;
 132    }
 133  10 if (level == null) {
 134  0 this.level = "1";
 135    } else {
 136  10 this.level = level;
 137    }
 138  10 this.printer = new PrintStream(outputStream);
 139  10 printLatexHeader();
 140  10 printQedeqHeader();
 141  10 printQedeqChapters();
 142  10 printQedeqBibliography();
 143  10 printLatexTrailer();
 144  10 if (printer.checkError()) {
 145  0 throw new IOException("TODO mime: better use another OutputStream");
 146    }
 147    }
 148   
 149    /**
 150    * Prints the header.
 151    */
 152  10 private void printQedeqHeader() {
 153  10 final LatexList title = qedeq.getHeader().getTitle();
 154  10 printer.print("\\title{");
 155  10 printer.print(getLatexListEntry(title));
 156  10 printer.println("}");
 157  10 printer.println("\\author{");
 158  10 final AuthorList authors = qedeq.getHeader().getAuthorList();
 159  10 for (int i = 0; i < authors.size(); i++) {
 160  10 final Author author = authors.get(i);
 161  10 printer.println(author.getName().getLatex());
 162    }
 163  10 printer.println("}");
 164  10 printer.println();
 165  10 printer.println("\\begin{document}");
 166  10 printer.println();
 167  10 printer.println("\\maketitle");
 168  10 printer.println();
 169  10 printer.println("\\setlength{\\parskip}{0pt}");
 170  10 printer.println("\\tableofcontents");
 171  10 printer.println("\\setlength{\\parskip}{5pt plus 2pt minus 1pt}");
 172  10 printer.println();
 173    }
 174   
 175    /**
 176    * Print all chapters.
 177    */
 178  10 private void printQedeqChapters() {
 179  10 final ChapterList chapters = qedeq.getChapterList();
 180  10 for (int i = 0; i < chapters.size(); i++) {
 181  50 final Chapter chapter = chapters.get(i);
 182  50 printer.print("\\chapter");
 183  50 if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) {
 184  16 printer.print("*");
 185    }
 186  50 printer.print("{");
 187  50 printer.print(getLatexListEntry(chapter.getTitle()));
 188  50 final String label = "chapter" + i;
 189  50 printer.println("} \\label{" + label + "} \\hypertarget{" + label + "}{}");
 190  50 if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) {
 191  16 printer.println("\\addcontentsline{toc}{chapter}{"
 192    + getLatexListEntry(chapter.getTitle()) + "}");
 193    }
 194  50 printer.println();
 195  50 if (chapter.getIntroduction() != null) {
 196  50 printer.println(getLatexListEntry(chapter.getIntroduction()));
 197  50 printer.println();
 198    }
 199  50 final SectionList sections = chapter.getSectionList();
 200  50 if (sections != null) {
 201  28 printSections(i, sections);
 202  28 printer.println();
 203    }
 204  50 printer.println("%% end of chapter " + getLatexListEntry(chapter.getTitle()));
 205  50 printer.println();
 206    }
 207    }
 208   
 209    /**
 210    * Print bibliography (if any).
 211    */
 212  10 private void printQedeqBibliography() {
 213  10 final LiteratureItemList items = qedeq.getLiteratureItemList();
 214  10 if (items == null) {
 215  6 return;
 216    }
 217  4 printer.println("\\begin{thebibliography}{99}");
 218  4 for (int i = 0; i < items.size(); i++) {
 219  18 final LiteratureItem item = items.get(i);
 220  18 printer.print("\\bibitem{" + item.getLabel() + "} ");
 221  18 printer.println(getLatexListEntry(item.getItem()));
 222  18 printer.println();
 223    }
 224  4 printer.println("\\end{thebibliography}");
 225    // TODO mime 20060926: remove language dependency
 226  4 if ("de".equals(language)) {
 227  2 printer.println("\\addcontentsline{toc}{chapter}{Literaturverzeichnis}");
 228    } else {
 229  2 printer.println("\\addcontentsline{toc}{chapter}{Bibliography}");
 230    }
 231   
 232    }
 233   
 234    /**
 235    * Print all given sections.
 236    *
 237    * @param chapter Chapter number.
 238    * @param sections List of sections.
 239    */
 240  28 private void printSections(final int chapter, final SectionList sections) {
 241  28 if (sections == null) {
 242  0 return;
 243    }
 244  28 for (int i = 0; i < sections.size(); i++) {
 245  84 final Section section = sections.get(i);
 246  84 printer.print("\\section{");
 247  84 printer.print(getLatexListEntry(section.getTitle()));
 248  84 final String label = "chapter" + chapter + "_section" + i;
 249  84 printer.println("} \\label{" + label + "} \\hypertarget{" + label + "}{}");
 250  84 printer.println(getLatexListEntry(section.getIntroduction()));
 251  84 printer.println();
 252  84 printSubsections(section.getSubsectionList());
 253    }
 254    }
 255   
 256    /**
 257    * Print all given subsections.
 258    *
 259    * @param nodes List of subsections.
 260    */
 261  84 private void printSubsections(final SubsectionList nodes) {
 262  84 if (nodes == null) {
 263  44 return;
 264    }
 265  40 for (int i = 0; i < nodes.size(); i++) {
 266  248 final SubsectionType subsectionType = nodes.get(i);
 267  248 if (subsectionType instanceof Node) {
 268  200 final Node node = (Node) subsectionType;
 269  200 printer.println("\\par");
 270  200 printer.println(getLatexListEntry(node.getPrecedingText()));
 271  200 printer.println();
 272  200 final String id = node.getId();
 273  200 final NodeType type = node.getNodeType();
 274  200 String title = null;
 275  200 if (node.getTitle() != null) {
 276  92 title = getLatexListEntry(node.getTitle());
 277    }
 278  200 if (type instanceof Axiom) {
 279  32 printAxiom((Axiom) type, title, id);
 280  168 } else if (type instanceof PredicateDefinition) {
 281  24 printPredicateDefinition((PredicateDefinition) type, title, id);
 282  144 } else if (type instanceof FunctionDefinition) {
 283  32 printFunctionDefinition((FunctionDefinition) type, title, id);
 284  112 } else if (type instanceof Proposition) {
 285  108 printProposition((Proposition) type, title, id);
 286  4 } else if (type instanceof Rule) {
 287  4 printRule((Rule) type, title, id);
 288    } else {
 289  0 throw new RuntimeException((type != null ? "unknown type: "
 290    + type.getClass().getName() : "node type empty"));
 291    }
 292  200 printer.println();
 293  200 printer.println(getLatexListEntry(node.getSucceedingText()));
 294    } else {
 295  48 final Subsection subsection = (Subsection) subsectionType;
 296  48 if (subsection.getTitle() != null) {
 297  42 printer.print("\\subsection{");
 298  42 printer.println(getLatexListEntry(subsection.getTitle()));
 299  42 printer.println("}");
 300    }
 301  48 printer.println(getLatexListEntry(subsection.getLatex()));
 302    }
 303  248 printer.println();
 304  248 printer.println();
 305    }
 306    }
 307   
 308    /**
 309    * Print axiom.
 310    *
 311    * @param axiom Print this.
 312    * @param title Extra name.
 313    * @param id Label for marking this axiom.
 314    */
 315  32 private void printAxiom(final Axiom axiom, final String title, final String id) {
 316  32 printer.println("\\begin{ax}" + (title != null ? "[" + title + "]" : ""));
 317  32 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 318  32 printFormula(axiom.getFormula().getElement());
 319  32 printer.println(getLatexListEntry(axiom.getDescription()));
 320  32 printer.println("\\end{ax}");
 321    }
 322   
 323    /**
 324    * Print top level formula. If the formula has the form <code>AND(.., .., ..)</code> the
 325    * formula is broken down in several labeled lines.
 326    *
 327    * @param element Formula to print.
 328    * @param mainLabel Main formula label.
 329    */
 330  108 private void printTopFormula(final Element element, final String mainLabel) {
 331  108 if (!element.isList() || !element.getList().getOperator().equals("AND")) {
 332  76 printFormula(element);
 333  76 return;
 334    }
 335  32 final ElementList list = element.getList();
 336  32 printer.println("\\mbox{}");
 337  32 printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{0.9\\linewidth}l}}");
 338  32 for (int i = 0; i < list.size(); i++) {
 339  158 final String label = (i < ALPHABET.length() ? "" + ALPHABET .charAt(i) : "" + i);
 340  158 printer.println("\\centering $" + getLatex(list.getElement(i)) + "$"
 341    + " & \\label{" + mainLabel + ":" + label + "} \\hypertarget{" + mainLabel + ":"
 342    + label + "}{} \\mbox{\\emph{(" + label + ")}} "
 343  158 + (i + 1 < list.size() ? "\\\\" : ""));
 344    }
 345  32 printer.println("\\end{longtable}");
 346    }
 347   
 348    /**
 349    * Print formula.
 350    *
 351    * @param element Formula to print.
 352    */
 353  108 private void printFormula(final Element element) {
 354  108 printer.println("\\mbox{}");
 355  108 printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{\\linewidth}}}");
 356  108 printer.println("\\centering $" + getLatex(element) + "$");
 357  108 printer.println("\\end{longtable}");
 358    }
 359   
 360    /**
 361    * Print predicate definition.
 362    *
 363    * @param definition Print this.
 364    * @param title Extra name.
 365    * @param id Label for marking this definition.
 366    */
 367  24 private void printPredicateDefinition(final PredicateDefinition definition, final String title,
 368    final String id) {
 369  24 final StringBuffer define = new StringBuffer("$$" + definition.getLatexPattern());
 370  24 final VariableList list = definition.getVariableList();
 371  24 if (list != null) {
 372  24 for (int i = list.size() - 1; i >= 0; i--) {
 373  38 Trace.trace(this, "printPredicateDefinition", "replacing!");
 374  38 ReplaceUtility.replace(define, "#" + (i + 1), getLatex(list.get(i)));
 375    }
 376    }
 377  24 if (definition.getFormula() != null) {
 378  20 printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : ""));
 379  20 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 380  20 define.append("\\ :\\leftrightarrow \\ ");
 381  20 define.append(getLatex(definition.getFormula().getElement()));
 382    } else {
 383  4 printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : ""));
 384  4 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 385    }
 386  24 define.append("$$");
 387  24 definitions.put(definition.getName() + "_" + definition.getArgumentNumber(), definition);
 388  24 Trace.param(this, "printPredicateDefinition", "define", define);
 389  24 printer.println(define);
 390  24 printer.println(getLatexListEntry(definition.getDescription()));
 391  24 if (definition.getFormula() != null) {
 392  20 printer.println("\\end{defn}");
 393    } else {
 394  4 printer.println("\\end{idefn}");
 395    }
 396    }
 397   
 398    /**
 399    * Print function definition.
 400    *
 401    * @param definition Print this.
 402    * @param title Extra name.
 403    * @param id Label for marking this definition.
 404    */
 405  32 private void printFunctionDefinition(final FunctionDefinition definition, final String title,
 406    final String id) {
 407  32 final StringBuffer define = new StringBuffer("$$" + definition.getLatexPattern());
 408  32 final VariableList list = definition.getVariableList();
 409  32 if (list != null) {
 410  26 for (int i = list.size() - 1; i >= 0; i--) {
 411  36 Trace.trace(this, "printFunctionDefinition", "replacing!");
 412  36 ReplaceUtility.replace(define, "#" + (i + 1), getLatex(list.get(i)));
 413    }
 414    }
 415  32 if (definition.getTerm() != null) {
 416  32 printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : ""));
 417  32 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 418  32 define.append("\\ := \\ ");
 419  32 define.append(getLatex(definition.getTerm().getElement()));
 420    } else {
 421  0 printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : ""));
 422  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 423    }
 424  32 define.append("$$");
 425  32 definitions.put(definition.getName() + "_" + definition.getArgumentNumber(), definition);
 426  32 Trace.param(this, "printFunctionDefinition", "define", define);
 427  32 printer.println(define);
 428  32 printer.println(getLatexListEntry(definition.getDescription()));
 429  32 if (definition.getTerm() != null) {
 430  32 printer.println("\\end{defn}");
 431    } else {
 432  0 printer.println("\\end{idefn}");
 433    }
 434    }
 435   
 436    /**
 437    * Print proposition.
 438    *
 439    * @param proposition Print this.
 440    * @param title Extra name.
 441    * @param id Label for marking this proposition.
 442    */
 443  108 private void printProposition(final Proposition proposition, final String title,
 444    final String id) {
 445  108 printer.println("\\begin{prop}" + (title != null ? "[" + title + "]" : ""));
 446  108 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 447  108 printTopFormula(proposition.getFormula().getElement(), id);
 448  108 printer.println(getLatexListEntry(proposition.getDescription()));
 449  108 printer.println("\\end{prop}");
 450  108 if (proposition.getProofList() != null) {
 451  10 for (int i = 0; i < proposition.getProofList().size(); i++) {
 452  10 printer.println("\\begin{proof}");
 453  10 printer.println(getLatexListEntry(proposition.getProofList().get(i)
 454    .getNonFormalProof()));
 455  10 printer.println("\\end{proof}");
 456    }
 457    }
 458    }
 459   
 460    /**
 461    * Print rule declaration.
 462    *
 463    * @param rule Print this.
 464    * @param title Extra name.
 465    * @param id Label for marking this proposition.
 466    */
 467  4 private void printRule(final Rule rule, final String title,
 468    final String id) {
 469  4 printer.println("\\begin{rul}" + (title != null ? "[" + title + "]" : ""));
 470  4 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 471  4 printer.println(getLatexListEntry(rule.getDescription()));
 472  4 printer.println("\\end{rul}");
 473   
 474    // TODO mime 20051210: are these informations equivalent to a formal proof?
 475    /*
 476    if (null != rule.getLinkList()) {
 477    printer.println("\\begin{proof}");
 478    printer.println("Rule name: " + rule.getName());
 479    printer.println();
 480    printer.println();
 481    for (int i = 0; i < rule.getLinkList().size(); i++) {
 482    printer.println(rule.getLinkList().get(i));
 483    }
 484    printer.println("\\end{proof}");
 485    }
 486    */
 487  4 if (rule.getProofList() != null) {
 488  0 for (int i = 0; i < rule.getProofList().size(); i++) {
 489  0 printer.println("\\begin{proof}");
 490  0 printer.println(getLatexListEntry(rule.getProofList().get(i)
 491    .getNonFormalProof()));
 492  0 printer.println("\\end{proof}");
 493    }
 494    }
 495    }
 496   
 497    /**
 498    * Get LaTeX element presentation.
 499    *
 500    * @param element Print this element.
 501    * @return LaTeX form of element.
 502    */
 503  392 private String getLatex(final Element element) {
 504  392 return getLatex(element, true);
 505    }
 506   
 507    /**
 508    * Get LaTeX element presentation.
 509    *
 510    * @param element Print this element.
 511    * @param first First level?
 512    * @return LaTeX form of element.
 513    */
 514  3036 private String getLatex(final Element element, final boolean first) {
 515  3036 final StringBuffer buffer = new StringBuffer();
 516  3036 if (element.isAtom()) {
 517  0 return element.getAtom().getString();
 518    }
 519  3036 final ElementList list = element.getList();
 520  3036 if (list.getOperator().equals("PREDCON")) {
 521  606 final String identifier = list.getElement(0).getAtom().getString() + "_"
 522    + (list.size() - 1);
 523    // TODO mime 20060922: is only working for definition name + argument number
 524    // if argument length is dynamic this dosen't work
 525  606 if (definitions.containsKey(identifier)) {
 526  606 final PredicateDefinition definition = (PredicateDefinition)
 527    definitions.get(identifier);
 528  606 final StringBuffer define = new StringBuffer(definition.getLatexPattern());
 529  606 for (int i = list.size() - 1; i >= 1; i--) {
 530  1038 ReplaceUtility.replace(define, "#" + i, getLatex(list.getElement(i), false));
 531    }
 532  606 buffer.append(define);
 533    } else {
 534  0 buffer.append(identifier);
 535  0 buffer.append("(");
 536  0 for (int i = 1; i < list.size(); i++) {
 537  0 buffer.append(getLatex(list.getElement(i), false));
 538  0 if (i + 1 < list.size()) {
 539  0 buffer.append(", ");
 540    }
 541    }
 542  0 buffer.append(")");
 543    }
 544  2430 } else if (list.getOperator().equals("PREDVAR")) {
 545  90 final String identifier = list.getElement(0).getAtom().getString();
 546  90 buffer.append(identifier);
 547  90 if (list.size() > 1) {
 548  42 buffer.append("(");
 549  42 for (int i = 1; i < list.size(); i++) {
 550  42 buffer.append(getLatex(list.getElement(i), false));
 551  42 if (i + 1 < list.size()) {
 552  0 buffer.append(", ");
 553    }
 554    }
 555  42 buffer.append(")");
 556    }
 557  2340 } else if (list.getOperator().equals("FUNCON")) {
 558  480 final String identifier = list.getElement(0).getAtom().getString() + "_"
 559    + (list.size() - 1);
 560    // TODO mime 20060922: is only working for definition name + argument number
 561    // if argument length is dynamic this dosen't work
 562  480 if (definitions.containsKey(identifier)) {
 563  480 final FunctionDefinition definition = (FunctionDefinition)
 564    definitions.get(identifier);
 565  480 final StringBuffer define = new StringBuffer(definition.getLatexPattern());
 566  480 for (int i = list.size() - 1; i >= 1; i--) {
 567  566 ReplaceUtility.replace(define, "#" + i, getLatex(list.getElement(i), false));
 568    }
 569  480 buffer.append(define);
 570    } else {
 571  0 buffer.append(identifier);
 572  0 buffer.append("(");
 573  0 for (int i = 1; i < list.size(); i++) {
 574  0 buffer.append(getLatex(list.getElement(i), false));
 575  0 if (i + 1 < list.size()) {
 576  0 buffer.append(", ");
 577    }
 578    }
 579  0 buffer.append(")");
 580    }
 581  1860 } else if (list.getOperator().equals("FUNVAR")) {
 582  0 final String identifier = list.getElement(0).getAtom().getString();
 583  0 buffer.append(identifier);
 584  0 if (list.size() > 1) {
 585  0 buffer.append("(");
 586  0 for (int i = 1; i < list.size(); i++) {
 587  0 buffer.append(getLatex(list.getElement(i), false));
 588  0 if (i + 1 < list.size()) {
 589  0 buffer.append(", ");
 590    }
 591    }
 592  0 buffer.append(")");
 593    }
 594  1860 } else if (list.getOperator().equals("VAR")) {
 595  1352 final String text = list.getElement(0).getAtom().getString();
 596    // interpret variable identifier as number
 597  1352 try {
 598  1352 final int index = Integer.parseInt(text);
 599  0 final String newText = "" + index;
 600  0 if (!text.equals(newText) || newText.startsWith("-")) {
 601  0 throw new NumberFormatException("This is no allowed number: " + text);
 602    }
 603  0 switch (index) {
 604  0 case 1:
 605  0 return "x";
 606  0 case 2:
 607  0 return "y";
 608  0 case 3:
 609  0 return "z";
 610  0 case 4:
 611  0 return "u";
 612  0 case 5:
 613  0 return "v";
 614  0 case 6:
 615  0 return "w";
 616  0 default:
 617  0 return "x_" + (index - 6);
 618    }
 619    } catch (NumberFormatException e) {
 620    // variable identifier is no number, just take it as it is
 621  1352 return text;
 622    }
 623  508 } else if (list.getOperator().equals("AND") || list.getOperator().equals("OR")
 624    || list.getOperator().equals("EQUI") || list.getOperator().equals("IMPL")) {
 625  330 final String infix;
 626  330 if (list.getOperator().equals("AND")) {
 627  80 infix = "\\ \\land \\ ";
 628  250 } else if (list.getOperator().equals("OR")) {
 629  30 infix = "\\ \\lor \\ ";
 630  220 } else if (list.getOperator().equals("EQUI")) {
 631  84 infix = "\\ \\leftrightarrow \\ ";
 632    } else {
 633  136 infix = "\\ \\rightarrow \\ ";
 634    }
 635  330 if (!first) {
 636  172 buffer.append("(");
 637    }
 638  330 for (int i = 0; i < list.size(); i++) {
 639  672 buffer.append(getLatex(list.getElement(i), false));
 640  672 if (i + 1 < list.size()) {
 641  342 buffer.append(infix);
 642    }
 643    }
 644  330 if (!first) {
 645  172 buffer.append(")");
 646    }
 647  178 } else if (list.getOperator().equals("FORALL") || list.getOperator().equals("EXISTS")
 648    || list.getOperator().equals("EXISTSU")) {
 649  84 final String prefix;
 650  84 if (list.getOperator().equals("FORALL")) {
 651  50 prefix = "\\forall ";
 652  34 } else if (list.getOperator().equals("EXISTS")) {
 653  28 prefix = "\\exists ";
 654    } else {
 655  6 prefix = "\\exists! ";
 656    }
 657  84 buffer.append(prefix);
 658  84 for (int i = 0; i < list.size(); i++) {
 659  172 if (i != 0 || (i == 0 && list.size() <= 2)) {
 660  168 buffer.append(getLatex(list.getElement(i), false));
 661    }
 662  172 if (i + 1 < list.size()) {
 663  88 buffer.append("\\ ");
 664    }
 665  172 if (list.size() > 2 && i == 1) {
 666  4 buffer.append("\\ ");
 667    }
 668    }
 669  94 } else if (list.getOperator().equals("NOT")) {
 670  30 final String prefix = "\\neg ";
 671  30 buffer.append(prefix);
 672  30 for (int i = 0; i < list.size(); i++) {
 673  30 buffer.append(getLatex(list.getElement(i), false));
 674    }
 675  64 } else if (list.getOperator().equals("CLASS")) {
 676  64 final String prefix = "\\{ ";
 677  64 buffer.append(prefix);
 678  64 for (int i = 0; i < list.size(); i++) {
 679  128 buffer.append(getLatex(list.getElement(i), false));
 680  128 if (i + 1 < list.size()) {
 681  64 buffer.append(" \\ | \\ ");
 682    }
 683    }
 684  64 buffer.append(" \\} ");
 685  0 } else if (list.getOperator().equals("CLASSLIST")) {
 686  0 final String prefix = "\\{ ";
 687  0 buffer.append(prefix);
 688  0 for (int i = 0; i < list.size(); i++) {
 689  0 buffer.append(getLatex(list.getElement(i), false));
 690  0 if (i + 1 < list.size()) {
 691  0 buffer.append(", \\ ");
 692    }
 693    }
 694  0 buffer.append(" \\} ");
 695  0 } else if (list.getOperator().equals("QUANTOR_INTERSECTION")) {
 696  0 final String prefix = "\\bigcap";
 697  0 buffer.append(prefix);
 698  0 if (0 < list.size()) {
 699  0 buffer.append("{").append(getLatex(list.getElement(0), false)).append("}");
 700    }
 701  0 for (int i = 1; i < list.size(); i++) {
 702  0 buffer.append(getLatex(list.getElement(i), false));
 703  0 if (i + 1 < list.size()) {
 704  0 buffer.append(" \\ \\ ");
 705    }
 706    }
 707  0 buffer.append(" \\} ");
 708  0 } else if (list.getOperator().equals("QUANTOR_UNION")) {
 709  0 final String prefix = "\\bigcup";
 710  0 buffer.append(prefix);
 711  0 if (0 < list.size()) {
 712  0 buffer.append("{").append(getLatex(list.getElement(0), false)).append("}");
 713    }
 714  0 for (int i = 1; i < list.size(); i++) {
 715  0 buffer.append(getLatex(list.getElement(i), false));
 716  0 if (i + 1 < list.size()) {
 717  0 buffer.append(" \\ \\ ");
 718    }
 719    }
 720  0 buffer.append(" \\} ");
 721    } else {
 722  0 buffer.append(list.getOperator());
 723  0 buffer.append("(");
 724  0 for (int i = 0; i < list.size(); i++) {
 725  0 buffer.append(getLatex(list.getElement(i), false));
 726  0 if (i + 1 < list.size()) {
 727  0 buffer.append(", ");
 728    }
 729    }
 730  0 buffer.append(")");
 731    }
 732  1684 return buffer.toString();
 733    }
 734   
 735    /**
 736    * Print LaTeX lines for the file head.
 737    */
 738  10 private void printLatexHeader() {
 739  10 printer.println("% -*- TeX:" + language.toUpperCase() + " -*-");
 740  10 printer.println("%%% ====================================================================");
 741  10 printer.println("%%% @LaTeX-file " + getFileName());
 742  10 printer.println("%%% Generated at " + getTimestamp());
 743  10 printer.println("%%% ====================================================================");
 744  10 printer.println();
 745  10 printer.println(
 746    "%%% Permission is granted to copy, distribute and/or modify this document");
 747  10 printer.println("%%% under the terms of the GNU Free Documentation License, Version 1.2");
 748  10 printer.println("%%% or any later version published by the Free Software Foundation;");
 749  10 printer.println(
 750    "%%% with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts.");
 751  10 printer.println();
 752  10 printer.println("\\documentclass[a4paper,german,10pt,twoside]{book}");
 753  10 if ("de".equals(language)) {
 754  5 printer.println("\\usepackage[german]{babel}");
 755  5 } else if ("en".equals(language)) {
 756  5 printer.println("\\usepackage[english]{babel}");
 757    } else {
 758  0 printer.println("%%% TODO unknown language: " + language);
 759  0 printer.println("%%% TODO using default language");
 760  0 printer.println("\\usepackage[english]{babel}");
 761    }
 762  10 printer.println("\\usepackage{makeidx}");
 763  10 printer.println("\\usepackage{amsmath,amsthm,amssymb}");
 764  10 printer.println("\\usepackage{color}");
 765  10 printer.println("\\usepackage[bookmarks,bookmarksnumbered,bookmarksopen,");
 766  10 printer.println(" colorlinks,linkcolor=webgreen,pagebackref]{hyperref}");
 767  10 printer.println("\\definecolor{webgreen}{rgb}{0,.5,0}");
 768  10 printer.println("\\usepackage{graphicx}");
 769  10 printer.println("\\usepackage{xr}");
 770  10 printer.println("\\usepackage{epsfig,longtable}");
 771  10 printer.println("\\usepackage{tabularx}");
 772  10 printer.println();
 773  10 if ("de".equals(language)) {
 774  5 printer.println("\\newtheorem{thm}{Theorem}[chapter]");
 775  5 printer.println("\\newtheorem{cor}[thm]{Korollar}");
 776  5 printer.println("\\newtheorem{lem}[thm]{Lemma}");
 777  5 printer.println("\\newtheorem{prop}[thm]{Proposition}");
 778  5 printer.println("\\newtheorem{ax}{Axiom}");
 779  5 printer.println("\\newtheorem{rul}{Regel}");
 780  5 printer.println();
 781  5 printer.println("\\theoremstyle{definition}");
 782  5 printer.println("\\newtheorem{defn}[thm]{Definition}");
 783  5 printer.println("\\newtheorem{idefn}[thm]{Initiale Definition}");
 784  5 printer.println();
 785  5 printer.println("\\theoremstyle{remark}");
 786  5 printer.println("\\newtheorem{rem}[thm]{Bemerkung}");
 787  5 printer.println("\\newtheorem*{notation}{Notation}");
 788  5 } else if ("en".equals(language)) {
 789  5 printer.println("\\newtheorem{thm}{Theorem}[chapter]");
 790  5 printer.println("\\newtheorem{cor}[thm]{Corollary}");
 791  5 printer.println("\\newtheorem{lem}[thm]{Lemma}");
 792  5 printer.println("\\newtheorem{prop}[thm]{Proposition}");
 793  5 printer.println("\\newtheorem{ax}{Axiom}");
 794  5 printer.println("\\newtheorem{rul}{Rule}");
 795  5 printer.println();
 796  5 printer.println("\\theoremstyle{definition}");
 797  5 printer.println("\\newtheorem{defn}[thm]{Definition}");
 798  5 printer.println("\\newtheorem{idefn}[thm]{Initial Definition}");
 799  5 printer.println();
 800  5 printer.println("\\theoremstyle{remark}");
 801  5 printer.println("\\newtheorem{rem}[thm]{Remark}");
 802  5 printer.println("\\newtheorem*{notation}{Notation}");
 803    } else {
 804  0 printer.println("%%% TODO unknown language: " + language);
 805  0 printer.println("%%% TODO using default language");
 806  0 printer.println("\\newtheorem{thm}{Theorem}[chapter]");
 807  0 printer.println("\\newtheorem{cor}[thm]{Corollary}");
 808  0 printer.println("\\newtheorem{lem}[thm]{Lemma}");
 809  0 printer.println("\\newtheorem{prop}[thm]{Proposition}");
 810  0 printer.println("\\newtheorem{ax}{Axiom}");
 811  0 printer.println();
 812  0 printer.println("\\theoremstyle{definition}");
 813  0 printer.println("\\newtheorem{defn}[thm]{Definition}");
 814  0 printer.println("\\newtheorem{idefn}[thm]{Initial Definition}");
 815  0 printer.println();
 816  0 printer.println("\\theoremstyle{remark}");
 817  0 printer.println("\\newtheorem{rem}[thm]{Remark}");
 818  0 printer.println("\\newtheorem*{notation}{Notation}");
 819    }
 820  10 printer.println();
 821  10 printer.println("\\addtolength{\\textheight}{7\\baselineskip}");
 822  10 printer.println("\\addtolength{\\topmargin}{-5\\baselineskip}");
 823  10 printer.println();
 824  10 printer.println("\\setlength{\\parindent}{0pt}");
 825  10 printer.println();
 826  10 printer.println("\\frenchspacing \\sloppy");
 827  10 printer.println();
 828  10 printer.println("\\makeindex");
 829  10 printer.println();
 830  10 printer.println();
 831    }
 832   
 833    /**
 834    * Print LaTeX trailer.
 835    */
 836  10 private void printLatexTrailer() {
 837  10 printer.println("\\backmatter");
 838  10 printer.println();
 839  10 printer.println("\\addcontentsline{toc}{chapter}{\\indexname} \\printindex");
 840  10 printer.println();
 841  10 printer.println("\\end{document}");
 842  10 printer.println();
 843    }
 844   
 845    /**
 846    * Get regular name for the LaTeX file.
 847    *
 848    * @return File name.
 849    */
 850  10 private String getFileName() {
 851    // FIXME mime 20050805: add language, validate with currently used file name e.g.
 852    // qedeq_basic_concept_en.tex
 853  10 return qedeq.getHeader().getSpecification().getName() + "_"
 854    + qedeq.getHeader().getSpecification().getRuleVersion() + ".tex";
 855    }
 856   
 857    /**
 858    * Get timestamp.
 859    *
 860    * @return Current timestamp.
 861    */
 862  10 private String getTimestamp() {
 863  10 final SimpleDateFormat formatter = new SimpleDateFormat("yyyy-MM-dd' 'HH:mm:ss,SSS");
 864  10 return formatter.format(new Date());
 865    }
 866   
 867    /**
 868    * Filters correct entry out of LaTeX list. Filter criterion is for example the correct
 869    * language.
 870    * TODO mime 20050205: filter level too?
 871    *
 872    * @param list List of LaTeX texts.
 873    * @return Filtered text.
 874    */
 875  1154 private String getLatexListEntry(final LatexList list) {
 876  1154 if (list == null) {
 877  354 return "";
 878    }
 879  800 for (int i = 0; i < list.size(); i++) {
 880  1075 if (language.equals(list.get(i).getLanguage())) {
 881  579 return getLatex(list.get(i));
 882    }
 883    }
 884    // assume entry with missing language as default
 885  221 for (int i = 0; i < list.size(); i++) {
 886  221 if (list.get(i).getLanguage() == null) {
 887  192 return getLatex(list.get(i));
 888    }
 889    }
 890  29 for (int i = 0; i < list.size(); i++) { // TODO mime 20050222: evaluate default?
 891  29 return "MISSING! OTHER: " + getLatex(list.get(i));
 892    }
 893  0 return "MISSING!";
 894    }
 895   
 896    /**
 897    * Get really LaTeX. Does some simple character replacements for umlauts.
 898    * TODO mime 20050205: filter more than German umlauts
 899    *
 900    * @param latex Unescaped text.
 901    * @return Really LaTeX.
 902    */
 903  800 private String getLatex(final Latex latex) {
 904  800 if (latex.getLatex() == null) {
 905  8 return "";
 906    }
 907  792 final StringBuffer buffer = new StringBuffer(latex.getLatex());
 908  792 IoUtility.deleteLineLeadingWhitespace(buffer);
 909  792 ReplaceUtility.replace(buffer, "\u00fc", "{\\\"u}");
 910  792 ReplaceUtility.replace(buffer, "\u00f6", "{\\\"o}");
 911  792 ReplaceUtility.replace(buffer, "\u00e4", "{\\\"a}");
 912  792 ReplaceUtility.replace(buffer, "\u00dc", "{\\\"U}");
 913  792 ReplaceUtility.replace(buffer, "\u00d6", "{\\\"O}");
 914  792 ReplaceUtility.replace(buffer, "\u00c4", "{\\\"A}");
 915  792 ReplaceUtility.replace(buffer, "\u00df", "{\\ss}");
 916  792 return buffer.toString();
 917    }
 918   
 919    }
 
CloverReport generated by Clover Code Coverage v1.3.10
Do Jan 11 2007 09:22:29 CET.		   Open Source License registered to the Hilbert II Project. This license of Clover is provided to support the development of Hilbert II only.