Clover coverage report - QedeqKernelSe Coverage Report
Coverage timestamp: Do Mai 10 2007 03:16:40 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 729   Methods: 17
NCLOC: 536   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
Qedeq2Wiki.java 0% 0% 0% 0%
coverage
 1    /* $Id: Qedeq2Wiki.java,v 1.6 2007/04/12 23:50:12 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.File;
 21    import java.io.FileOutputStream;
 22    import java.io.IOException;
 23    import java.io.OutputStream;
 24    import java.io.PrintStream;
 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.Axiom;
 31    import org.qedeq.kernel.base.module.Chapter;
 32    import org.qedeq.kernel.base.module.ChapterList;
 33    import org.qedeq.kernel.base.module.FunctionDefinition;
 34    import org.qedeq.kernel.base.module.Latex;
 35    import org.qedeq.kernel.base.module.LatexList;
 36    import org.qedeq.kernel.base.module.LiteratureItem;
 37    import org.qedeq.kernel.base.module.LiteratureItemList;
 38    import org.qedeq.kernel.base.module.Node;
 39    import org.qedeq.kernel.base.module.NodeType;
 40    import org.qedeq.kernel.base.module.PredicateDefinition;
 41    import org.qedeq.kernel.base.module.Proposition;
 42    import org.qedeq.kernel.base.module.Qedeq;
 43    import org.qedeq.kernel.base.module.Rule;
 44    import org.qedeq.kernel.base.module.Section;
 45    import org.qedeq.kernel.base.module.SectionList;
 46    import org.qedeq.kernel.base.module.Subsection;
 47    import org.qedeq.kernel.base.module.SubsectionList;
 48    import org.qedeq.kernel.base.module.SubsectionType;
 49    import org.qedeq.kernel.base.module.VariableList;
 50    import org.qedeq.kernel.bo.module.ModuleDataException;
 51    import org.qedeq.kernel.bo.module.QedeqBo;
 52    import org.qedeq.kernel.dto.module.PredicateDefinitionVo;
 53    import org.qedeq.kernel.trace.Trace;
 54    import org.qedeq.kernel.utility.ReplaceUtility;
 55   
 56   
 57    /**
 58    * Transfer a qedeq module into text files in MediaWiki format.
 59    * <p>
 60    * FIXME mime 20060831: This is just a quick hacked generator. This class just
 61    * generates some text files.
 62    * <p>
 63    * <b>It is not finished!</b>
 64    * <p>
 65    * It should be compared with Qedeq2Latex and then refactored to reuse common functions.
 66    *
 67    * @version $Revision: 1.6 $
 68    * @author Michael Meyling
 69    */
 70    public final class Qedeq2Wiki {
 71   
 72    /** Alphabet for tagging. */
 73    private static final String ALPHABET = "abcdefghijklmnopqrstuvwxyz";
 74   
 75    /** Output goes here. */
 76    private PrintStream printer;
 77   
 78    /** QEDEQ module to transfer into WIKI form. */
 79    private Qedeq qedeq;
 80   
 81    /** Filter text to get and produce text in this language. */
 82    private String language;
 83   
 84    /** Filter for this detail level. TODO mime 20050205: not used yet. */
 85    private String level;
 86   
 87    /** Maps identifiers to {@link PredicateDefinition}s. */
 88    private Map definitions = new HashMap();
 89   
 90    /** Destination directory. */
 91    private File outputDirectory;
 92   
 93    /**
 94    * Constructor.
 95    *
 96    * @param context Context within this module is created.
 97    * @param qedeq Work with this QEDEQ module.
 98    * @throws ModuleDataException
 99    */
 100  0 public Qedeq2Wiki(final String context, final QedeqBo qedeq) throws ModuleDataException {
 101  0 this.qedeq = qedeq;
 102  0 final PredicateDefinitionVo equal = new PredicateDefinitionVo();
 103    // LATER mime 20050224: quick hack to have the logical identity operator
 104  0 equal.setArgumentNumber("2");
 105  0 equal.setLatexPattern("#1 \\ = \\ #2");
 106  0 definitions.put("equal", equal);
 107    // LATER mime 20060822: quick hack to get the negation of the logical identity operator
 108  0 final PredicateDefinitionVo notEqual = new PredicateDefinitionVo();
 109  0 notEqual.setArgumentNumber("2");
 110  0 notEqual.setLatexPattern("#1 \\ \\neq \\ #2");
 111  0 definitions.put("notEqual", notEqual);
 112    }
 113   
 114    /**
 115    * Prints a LaTeX file into a given output stream.
 116    *
 117    * @param language Filter text to get and produce text in this language only.
 118    * @param level Filter for this detail level. TODO mime 20050205: not supported yet.
 119    * @param outputDirectory Write files to this directory.
 120    * @throws IOException
 121    */
 122  0 public final synchronized void printWiki(final String language, final String level,
 123    final File outputDirectory) throws IOException {
 124  0 if (language == null) {
 125  0 this.language = "en";
 126    } else {
 127  0 this.language = language;
 128    }
 129  0 if (level == null) {
 130  0 this.level = "1";
 131    } else {
 132  0 this.level = level;
 133    }
 134  0 this.outputDirectory = outputDirectory;
 135  0 printQedeqChapters();
 136  0 printQedeqBibliography();
 137  0 if (printer.checkError()) {
 138  0 throw new IOException("TODO mime: better use another OutputStream");
 139    }
 140    }
 141   
 142    /**
 143    * Print all chapters.
 144    *
 145    * @throws IOException Writing failed.
 146    */
 147  0 private void printQedeqChapters() throws IOException {
 148  0 final ChapterList chapters = qedeq.getChapterList();
 149  0 for (int i = 0; i < chapters.size(); i++) {
 150  0 final String label = qedeq.getHeader().getSpecification().getName() + "_ch_" + i;
 151  0 final OutputStream outputStream = new FileOutputStream(new File(outputDirectory,
 152    label + "_" + language + ".wiki"));
 153  0 this.printer = new PrintStream(outputStream);
 154  0 final Chapter chapter = chapters.get(i);
 155  0 printer.print("\\chapter");
 156  0 if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) {
 157  0 printer.print("*");
 158    }
 159  0 printer.println("== " + getLatexListEntry(chapter.getTitle()) + " ==");
 160  0 printer.println();
 161  0 printer.println("<div id=\"" + label + "\"></div>");
 162    // if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) {
 163  0 printer.println();
 164  0 if (chapter.getIntroduction() != null) {
 165  0 printer.println(getLatexListEntry(chapter.getIntroduction()));
 166  0 printer.println();
 167    }
 168  0 final SectionList sections = chapter.getSectionList();
 169  0 if (sections != null) {
 170  0 printSections(i, sections);
 171  0 printer.println();
 172    }
 173  0 printer.println("%% end of chapter " + getLatexListEntry(chapter.getTitle()));
 174  0 printer.println();
 175    }
 176    }
 177   
 178    /**
 179    * Print bibliography (if any).
 180    */
 181  0 private void printQedeqBibliography() {
 182  0 final LiteratureItemList items = qedeq.getLiteratureItemList();
 183  0 if (items == null) {
 184  0 return;
 185    }
 186  0 printer.println("\\begin{thebibliography}{99}");
 187  0 for (int i = 0; i < items.size(); i++) {
 188  0 final LiteratureItem item = items.get(i);
 189  0 printer.print("\\bibitem{" + item.getLabel() + "} ");
 190  0 printer.println(getLatexListEntry(item.getItem()));
 191  0 printer.println();
 192    }
 193  0 printer.println("\\end{thebibliography}");
 194  0 printer.println("\\addcontentsline{toc}{chapter}{Literaturverzeichnis}");
 195    }
 196   
 197    /**
 198    * Print all given sections.
 199    *
 200    * @param chapter Chapter number.
 201    * @param sections List of sections.
 202    */
 203  0 private void printSections(final int chapter, final SectionList sections) {
 204  0 if (sections == null) {
 205  0 return;
 206    }
 207  0 for (int i = 0; i < sections.size(); i++) {
 208  0 final Section section = sections.get(i);
 209  0 printer.print("\\section{");
 210  0 printer.print(getLatexListEntry(section.getTitle()));
 211  0 final String label = "chapter" + chapter + "_section" + i;
 212  0 printer.println("} \\label{" + label + "} \\hypertarget{" + label + "}{}");
 213  0 printer.println(getLatexListEntry(section.getIntroduction()));
 214  0 printer.println();
 215  0 printSubsections(section.getSubsectionList());
 216    }
 217    }
 218   
 219    /**
 220    * Print all given subsections.
 221    *
 222    * @param nodes List of subsections.
 223    */
 224  0 private void printSubsections(final SubsectionList nodes) {
 225  0 if (nodes == null) {
 226  0 return;
 227    }
 228  0 for (int i = 0; i < nodes.size(); i++) {
 229  0 final SubsectionType subsectionType = nodes.get(i);
 230  0 if (subsectionType instanceof Node) {
 231  0 final Node node = (Node) subsectionType;
 232  0 printer.println(getLatexListEntry(node.getPrecedingText()));
 233  0 printer.println();
 234  0 printer.println("\\par");
 235  0 final String id = node.getId();
 236  0 final NodeType type = node.getNodeType();
 237  0 String title = null;
 238  0 if (node.getTitle() != null) {
 239  0 title = getLatexListEntry(node.getTitle());
 240    }
 241  0 if (type instanceof Axiom) {
 242  0 printAxiom((Axiom) type, title, id);
 243  0 } else if (type instanceof PredicateDefinition) {
 244  0 printPredicateDefinition((PredicateDefinition) type, title, id);
 245  0 } else if (type instanceof FunctionDefinition) {
 246  0 printFunctionDefinition((FunctionDefinition) type, title, id);
 247  0 } else if (type instanceof Proposition) {
 248  0 printProposition((Proposition) type, title, id);
 249  0 } else if (type instanceof Rule) {
 250  0 printRule((Rule) type, title, id);
 251    } else {
 252  0 throw new RuntimeException((type != null ? "unknown type: "
 253    + type.getClass().getName() : "node type empty"));
 254    }
 255  0 printer.println();
 256  0 printer.println(getLatexListEntry(node.getSucceedingText()));
 257    } else {
 258  0 final Subsection subsection = (Subsection) subsectionType;
 259  0 if (subsection.getTitle() != null) {
 260  0 printer.print("\\subsection{");
 261  0 printer.println(getLatexListEntry(subsection.getTitle()));
 262  0 printer.println("}");
 263    }
 264  0 printer.println(getLatexListEntry(subsection.getLatex()));
 265    }
 266  0 printer.println();
 267  0 printer.println();
 268    }
 269    }
 270   
 271    /**
 272    * Print axiom.
 273    *
 274    * @param axiom Print this.
 275    * @param title Extra name.
 276    * @param id Label for marking this axiom.
 277    */
 278  0 private void printAxiom(final Axiom axiom, final String title, final String id) {
 279  0 printer.println("\\begin{ax}" + (title != null ? "[" + title + "]" : ""));
 280  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 281  0 printFormula(axiom.getFormula().getElement());
 282  0 printer.println(getLatexListEntry(axiom.getDescription()));
 283  0 printer.println("\\end{ax}");
 284    }
 285   
 286    /**
 287    * Print top level formula. If the formula has the form <code>AND(.., .., ..)</code> the
 288    * formula is broken down in several labeled lines.
 289    *
 290    * @param element Formula to print.
 291    * @param mainLabel Main formula label.
 292    */
 293  0 private void printTopFormula(final Element element, final String mainLabel) {
 294  0 if (!element.isList() || !element.getList().getOperator().equals("AND")) {
 295  0 printFormula(element);
 296  0 return;
 297    }
 298  0 final ElementList list = element.getList();
 299  0 printer.println("\\mbox{}");
 300  0 printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{0.9\\linewidth}l}}");
 301  0 for (int i = 0; i < list.size(); i++) {
 302  0 final String label = (i < ALPHABET.length() ? "" + ALPHABET .charAt(i) : "" + i);
 303  0 printer.println("\\centering $" + getLatex(list.getElement(i)) + "$"
 304    + " & \\label{" + mainLabel + ":" + label + "} \\hypertarget{" + mainLabel + ":"
 305    + label + "}{} \\mbox{\\emph{(" + label + ")}} "
 306  0 + (i + 1 < list.size() ? "\\\\" : ""));
 307    }
 308  0 printer.println("\\end{longtable}");
 309    }
 310   
 311    /**
 312    * Print formula.
 313    *
 314    * @param element Formula to print.
 315    */
 316  0 private void printFormula(final Element element) {
 317  0 printer.println("\\mbox{}");
 318  0 printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{\\linewidth}}}");
 319  0 printer.println("\\centering $" + getLatex(element) + "$");
 320  0 printer.println("\\end{longtable}");
 321    }
 322   
 323    /**
 324    * Print predicate definition.
 325    *
 326    * @param definition Print this.
 327    * @param title Extra name.
 328    * @param id Label for marking this definition.
 329    */
 330  0 private void printPredicateDefinition(final PredicateDefinition definition, final String title,
 331    final String id) {
 332  0 final StringBuffer define = new StringBuffer("$$" + definition.getLatexPattern());
 333  0 final VariableList list = definition.getVariableList();
 334  0 if (list != null) {
 335  0 for (int i = list.size() - 1; i >= 0; i--) {
 336  0 Trace.trace(this, "printDefinition", "replacing!");
 337  0 ReplaceUtility.replace(define, "#" + (i + 1), getLatex(list.get(i)));
 338    }
 339    }
 340  0 if (definition.getFormula() != null) {
 341  0 printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : ""));
 342  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 343  0 define.append("\\ :\\leftrightarrow \\ ");
 344  0 define.append(getLatex(definition.getFormula().getElement()));
 345    } else {
 346  0 printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : ""));
 347  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 348    }
 349  0 define.append("$$");
 350  0 definitions.put(id, definition);
 351  0 Trace.param(this, "printDefinition", "define", define);
 352  0 printer.println(define);
 353  0 printer.println(getLatexListEntry(definition.getDescription()));
 354  0 if (definition.getFormula() != null) {
 355  0 printer.println("\\end{defn}");
 356    } else {
 357  0 printer.println("\\end{idefn}");
 358    }
 359    }
 360   
 361    /**
 362    * Print function definition.
 363    *
 364    * @param definition Print this.
 365    * @param title Extra name.
 366    * @param id Label for marking this definition.
 367    */
 368  0 private void printFunctionDefinition(final FunctionDefinition definition, final String title,
 369    final String id) {
 370  0 final StringBuffer define = new StringBuffer("$$" + definition.getLatexPattern());
 371  0 final VariableList list = definition.getVariableList();
 372  0 if (list != null) {
 373  0 for (int i = list.size() - 1; i >= 0; i--) {
 374  0 Trace.trace(this, "printDefinition", "replacing!");
 375  0 ReplaceUtility.replace(define, "#" + (i + 1), getLatex(list.get(i)));
 376    }
 377    }
 378  0 if (definition.getTerm() != null) {
 379  0 printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : ""));
 380  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 381  0 define.append("\\ := \\ ");
 382  0 define.append(getLatex(definition.getTerm().getElement()));
 383    } else {
 384  0 printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : ""));
 385  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 386    }
 387  0 define.append("$$");
 388  0 definitions.put(id, definition);
 389  0 Trace.param(this, "printDefinition", "define", define);
 390  0 printer.println(define);
 391  0 printer.println(getLatexListEntry(definition.getDescription()));
 392  0 if (definition.getTerm() != null) {
 393  0 printer.println("\\end{defn}");
 394    } else {
 395  0 printer.println("\\end{idefn}");
 396    }
 397    }
 398   
 399    /**
 400    * Print proposition.
 401    *
 402    * @param proposition Print this.
 403    * @param title Extra name.
 404    * @param id Label for marking this proposition.
 405    */
 406  0 private void printProposition(final Proposition proposition, final String title,
 407    final String id) {
 408  0 printer.println("\\begin{prop}" + (title != null ? "[" + title + "]" : ""));
 409  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 410  0 printTopFormula(proposition.getFormula().getElement(), id);
 411  0 printer.println(getLatexListEntry(proposition.getDescription()));
 412  0 printer.println("\\end{prop}");
 413  0 if (proposition.getProofList() != null) {
 414  0 for (int i = 0; i < proposition.getProofList().size(); i++) {
 415  0 printer.println("\\begin{proof}");
 416  0 printer.println(getLatexListEntry(proposition.getProofList().get(i)
 417    .getNonFormalProof()));
 418  0 printer.println("\\end{proof}");
 419    }
 420    }
 421    }
 422   
 423    /**
 424    * Print rule declaration.
 425    *
 426    * @param rule Print this.
 427    * @param title Extra name.
 428    * @param id Label for marking this proposition.
 429    */
 430  0 private void printRule(final Rule rule, final String title,
 431    final String id) {
 432  0 printer.println("\\begin{rul}" + (title != null ? "[" + title + "]" : ""));
 433  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 434  0 printer.println(getLatexListEntry(rule.getDescription()));
 435  0 printer.println("\\end{rul}");
 436   
 437    // TODO mime 20051210: are these informations equivalent to a formal proof?
 438    /*
 439    if (null != rule.getLinkList()) {
 440    printer.println("\\begin{proof}");
 441    printer.println("Rule name: " + rule.getName());
 442    printer.println();
 443    printer.println();
 444    for (int i = 0; i < rule.getLinkList().size(); i++) {
 445    printer.println(rule.getLinkList().get(i));
 446    }
 447    printer.println("\\end{proof}");
 448    }
 449    */
 450  0 if (rule.getProofList() != null) {
 451  0 for (int i = 0; i < rule.getProofList().size(); i++) {
 452  0 printer.println("\\begin{proof}");
 453  0 printer.println(getLatexListEntry(rule.getProofList().get(i)
 454    .getNonFormalProof()));
 455  0 printer.println("\\end{proof}");
 456    }
 457    }
 458    }
 459   
 460    /**
 461    * Get LaTeX element presentation.
 462    *
 463    * @param element Print this element.
 464    * @return LaTeX form of element.
 465    */
 466  0 private String getLatex(final Element element) {
 467  0 return getLatex(element, true);
 468    }
 469   
 470    /**
 471    * Get LaTeX element presentation.
 472    *
 473    * @param element Print this element.
 474    * @param first First level?
 475    * @return LaTeX form of element.
 476    */
 477  0 private String getLatex(final Element element, final boolean first) {
 478  0 final StringBuffer buffer = new StringBuffer();
 479  0 if (element.isAtom()) {
 480  0 return element.getAtom().getString();
 481    }
 482  0 final ElementList list = element.getList();
 483  0 if (list.getOperator().equals("PREDCON")) {
 484  0 final String identifier = list.getElement(0).getAtom().getString();
 485  0 if (definitions.containsKey(identifier)) {
 486  0 final PredicateDefinition definition
 487    = (PredicateDefinition) definitions.get(identifier);
 488  0 final StringBuffer define = new StringBuffer(definition.getLatexPattern());
 489  0 for (int i = list.size() - 1; i >= 1; i--) {
 490  0 ReplaceUtility.replace(define, "#" + i, getLatex(list.getElement(i), false));
 491    }
 492  0 buffer.append(define);
 493    } else {
 494  0 buffer.append(identifier);
 495  0 buffer.append("(");
 496  0 for (int i = 1; i < list.size(); i++) {
 497  0 buffer.append(getLatex(list.getElement(i), false));
 498  0 if (i + 1 < list.size()) {
 499  0 buffer.append(", ");
 500    }
 501    }
 502  0 buffer.append(")");
 503    }
 504  0 } else if (list.getOperator().equals("PREDVAR")) {
 505  0 final String identifier = list.getElement(0).getAtom().getString();
 506  0 buffer.append(identifier);
 507  0 if (list.size() > 1) {
 508  0 buffer.append("(");
 509  0 for (int i = 1; i < list.size(); i++) {
 510  0 buffer.append(getLatex(list.getElement(i), false));
 511  0 if (i + 1 < list.size()) {
 512  0 buffer.append(", ");
 513    }
 514    }
 515  0 buffer.append(")");
 516    }
 517  0 } else if (list.getOperator().equals("FUNCON")) {
 518  0 final String identifier = list.getElement(0).getAtom().getString();
 519  0 if (definitions.containsKey(identifier)) {
 520  0 final FunctionDefinition definition
 521    = (FunctionDefinition) definitions.get(identifier);
 522  0 final StringBuffer define = new StringBuffer(definition.getLatexPattern());
 523  0 for (int i = list.size() - 1; i >= 1; i--) {
 524  0 ReplaceUtility.replace(define, "#" + i, getLatex(list.getElement(i), false));
 525    }
 526  0 buffer.append(define);
 527    } else {
 528  0 buffer.append(identifier);
 529  0 buffer.append("(");
 530  0 for (int i = 1; i < list.size(); i++) {
 531  0 buffer.append(getLatex(list.getElement(i), false));
 532  0 if (i + 1 < list.size()) {
 533  0 buffer.append(", ");
 534    }
 535    }
 536  0 buffer.append(")");
 537    }
 538  0 } else if (list.getOperator().equals("FUNVAR")) {
 539  0 final String identifier = list.getElement(0).getAtom().getString();
 540  0 buffer.append(identifier);
 541  0 if (list.size() > 1) {
 542  0 buffer.append("(");
 543  0 for (int i = 1; i < list.size(); i++) {
 544  0 buffer.append(getLatex(list.getElement(i), false));
 545  0 if (i + 1 < list.size()) {
 546  0 buffer.append(", ");
 547    }
 548    }
 549  0 buffer.append(")");
 550    }
 551  0 } else if (list.getOperator().equals("VAR")) {
 552  0 final String text = list.getElement(0).getAtom().getString();
 553  0 try {
 554  0 final int index = Integer.parseInt(text);
 555  0 switch (index) {
 556  0 case 1:
 557  0 return "x";
 558  0 case 2:
 559  0 return "y";
 560  0 case 3:
 561  0 return "z";
 562  0 case 4:
 563  0 return "u";
 564  0 case 5:
 565  0 return "v";
 566  0 case 6:
 567  0 return "w";
 568  0 default:
 569  0 return "x_" + (index - 6);
 570    }
 571    } catch (NumberFormatException e) {
 572  0 return text;
 573    }
 574  0 } else if (list.getOperator().equals("AND") || list.getOperator().equals("OR")
 575    || list.getOperator().equals("EQUI") || list.getOperator().equals("IMPL")) {
 576  0 final String infix;
 577  0 if (list.getOperator().equals("AND")) {
 578  0 infix = "\\ \\land \\ ";
 579  0 } else if (list.getOperator().equals("OR")) {
 580  0 infix = "\\ \\lor \\ ";
 581  0 } else if (list.getOperator().equals("EQUI")) {
 582  0 infix = "\\ \\leftrightarrow \\ ";
 583    } else {
 584  0 infix = "\\ \\rightarrow \\ ";
 585    }
 586  0 if (!first) {
 587  0 buffer.append("(");
 588    }
 589  0 for (int i = 0; i < list.size(); i++) {
 590  0 buffer.append(getLatex(list.getElement(i), false));
 591  0 if (i + 1 < list.size()) {
 592  0 buffer.append(infix);
 593    }
 594    }
 595  0 if (!first) {
 596  0 buffer.append(")");
 597    }
 598  0 } else if (list.getOperator().equals("FORALL") || list.getOperator().equals("EXISTS")
 599    || list.getOperator().equals("EXISTSU")) {
 600  0 final String prefix;
 601  0 if (list.getOperator().equals("FORALL")) {
 602  0 prefix = "\\forall ";
 603  0 } else if (list.getOperator().equals("EXISTS")) {
 604  0 prefix = "\\exists ";
 605    } else {
 606  0 prefix = "\\exists! ";
 607    }
 608  0 buffer.append(prefix);
 609  0 for (int i = 0; i < list.size(); i++) {
 610  0 if (i != 0 || (i == 0 && list.size() <= 2)) {
 611  0 buffer.append(getLatex(list.getElement(i), false));
 612    }
 613  0 if (i + 1 < list.size()) {
 614  0 buffer.append("\\ ");
 615    }
 616  0 if (list.size() > 2 && i == 1) {
 617  0 buffer.append("\\ ");
 618    }
 619    }
 620  0 } else if (list.getOperator().equals("NOT")) {
 621  0 final String prefix = "\\neg ";
 622  0 buffer.append(prefix);
 623  0 for (int i = 0; i < list.size(); i++) {
 624  0 buffer.append(getLatex(list.getElement(i), false));
 625    }
 626  0 } else if (list.getOperator().equals("CLASS")) {
 627  0 final String prefix = "\\{ ";
 628  0 buffer.append(prefix);
 629  0 for (int i = 0; i < list.size(); i++) {
 630  0 buffer.append(getLatex(list.getElement(i), false));
 631  0 if (i + 1 < list.size()) {
 632  0 buffer.append(" \\ | \\ ");
 633    }
 634    }
 635  0 buffer.append(" \\} ");
 636  0 } else if (list.getOperator().equals("CLASSLIST")) {
 637  0 final String prefix = "\\{ ";
 638  0 buffer.append(prefix);
 639  0 for (int i = 0; i < list.size(); i++) {
 640  0 buffer.append(getLatex(list.getElement(i), false));
 641  0 if (i + 1 < list.size()) {
 642  0 buffer.append(", \\ ");
 643    }
 644    }
 645  0 buffer.append(" \\} ");
 646  0 } else if (list.getOperator().equals("QUANTOR_INTERSECTION")) {
 647  0 final String prefix = "\\bigcap";
 648  0 buffer.append(prefix);
 649  0 if (0 < list.size()) {
 650  0 buffer.append("{").append(getLatex(list.getElement(0), false)).append("}");
 651    }
 652  0 for (int i = 1; i < list.size(); i++) {
 653  0 buffer.append(getLatex(list.getElement(i), false));
 654  0 if (i + 1 < list.size()) {
 655  0 buffer.append(" \\ \\ ");
 656    }
 657    }
 658  0 buffer.append(" \\} ");
 659  0 } else if (list.getOperator().equals("QUANTOR_UNION")) {
 660  0 final String prefix = "\\bigcup";
 661  0 buffer.append(prefix);
 662  0 if (0 < list.size()) {
 663  0 buffer.append("{").append(getLatex(list.getElement(0), false)).append("}");
 664    }
 665  0 for (int i = 1; i < list.size(); i++) {
 666  0 buffer.append(getLatex(list.getElement(i), false));
 667  0 if (i + 1 < list.size()) {
 668  0 buffer.append(" \\ \\ ");
 669    }
 670    }
 671  0 buffer.append(" \\} ");
 672    } else {
 673  0 buffer.append(list.getOperator());
 674  0 buffer.append("(");
 675  0 for (int i = 0; i < list.size(); i++) {
 676  0 buffer.append(getLatex(list.getElement(i), false));
 677  0 if (i + 1 < list.size()) {
 678  0 buffer.append(", ");
 679    }
 680    }
 681  0 buffer.append(")");
 682    }
 683  0 return buffer.toString();
 684    }
 685   
 686    /**
 687    * Filters correct entry out of LaTeX list. Filter criterion is for example the correct
 688    * language.
 689    * TODO mime 20050205: filter level too?
 690    *
 691    * @param list List of LaTeX texts.
 692    * @return Filtered text.
 693    */
 694  0 private String getLatexListEntry(final LatexList list) {
 695  0 if (list == null) {
 696  0 return "";
 697    }
 698  0 for (int i = 0; i < list.size(); i++) {
 699  0 if (language.equals(list.get(i).getLanguage())) {
 700  0 return getLatex(list.get(i));
 701    }
 702    }
 703    // assume entry with missing language as default
 704  0 for (int i = 0; i < list.size(); i++) {
 705  0 if (list.get(i).getLanguage() == null) {
 706  0 return getLatex(list.get(i));
 707    }
 708    }
 709  0 for (int i = 0; i < list.size(); i++) { // LATER mime 20050222: evaluate default?
 710  0 return "MISSING! OTHER: " + getLatex(list.get(i));
 711    }
 712  0 return "MISSING!";
 713    }
 714   
 715    /**
 716    * Get really LaTeX. Does some simple character replacements for umlauts.
 717    * TODO mime 20050205: filter more than German umlauts
 718    *
 719    * @param latex Unescaped text.
 720    * @return Really LaTeX.
 721    */
 722  0 private String getLatex(final Latex latex) {
 723  0 if (latex == null || latex.getLatex() == null) {
 724  0 return "";
 725    }
 726  0 return LatexTextParser.transform(latex.getLatex());
 727    }
 728   
 729    }
 
CloverReport generated by Clover Code Coverage v1.3.10
Do Mai 10 2007 04:02:49 CEST.		   Open Source License registered to the Hilbert II Project. This license of Clover is provided to support the development of Hilbert II only.