Clover coverage report - QedeqKernelSe Coverage Report
Coverage timestamp: Sa Jan 26 2008 14:11:34 CET
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 494   Methods: 16
NCLOC: 313   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
Qedeq2Wiki.java 0% 0% 0% 0%
coverage
 1    /* $Id: Qedeq2Wiki.java,v 1.9 2008/01/26 12:39:09 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   
 26    import org.qedeq.kernel.base.list.Element;
 27    import org.qedeq.kernel.base.list.ElementList;
 28    import org.qedeq.kernel.base.module.Axiom;
 29    import org.qedeq.kernel.base.module.Chapter;
 30    import org.qedeq.kernel.base.module.ChapterList;
 31    import org.qedeq.kernel.base.module.FunctionDefinition;
 32    import org.qedeq.kernel.base.module.Latex;
 33    import org.qedeq.kernel.base.module.LatexList;
 34    import org.qedeq.kernel.base.module.LiteratureItem;
 35    import org.qedeq.kernel.base.module.LiteratureItemList;
 36    import org.qedeq.kernel.base.module.Node;
 37    import org.qedeq.kernel.base.module.NodeType;
 38    import org.qedeq.kernel.base.module.PredicateDefinition;
 39    import org.qedeq.kernel.base.module.Proposition;
 40    import org.qedeq.kernel.base.module.Rule;
 41    import org.qedeq.kernel.base.module.Section;
 42    import org.qedeq.kernel.base.module.SectionList;
 43    import org.qedeq.kernel.base.module.Subsection;
 44    import org.qedeq.kernel.base.module.SubsectionList;
 45    import org.qedeq.kernel.base.module.SubsectionType;
 46    import org.qedeq.kernel.base.module.VariableList;
 47    import org.qedeq.kernel.bo.module.ModuleProperties;
 48    import org.qedeq.kernel.trace.Trace;
 49    import org.qedeq.kernel.utility.ReplaceUtility;
 50   
 51   
 52    /**
 53    * Transfer a QEDEQ module into text files in MediaWiki format.
 54    * <p>
 55    * LATER mime 20060831: This is just a quick hacked generator. This class just
 56    * generates some text files.
 57    * <p>
 58    * <b>It is not finished!</b>
 59    * <p>
 60    * It should be compared with Qedeq2Latex and then refactored to reuse common functions.
 61    *
 62    * @version $Revision: 1.9 $
 63    * @author Michael Meyling
 64    */
 65    public final class Qedeq2Wiki {
 66   
 67    /** This class. */
 68    private static final Class CLASS = Qedeq2Wiki.class;
 69   
 70    /** Alphabet for tagging. */
 71    private static final String ALPHABET = "abcdefghijklmnopqrstuvwxyz";
 72   
 73    /** QEDEQ module properties object to work on. */
 74    private final ModuleProperties prop;
 75   
 76    /** Output goes here. */
 77    private PrintStream printer;
 78   
 79    /** Filter text to get and produce text in this language. */
 80    private String language;
 81   
 82    /** Transformer to get LaTeX out of {@link Element}s. */
 83    private final Element2Latex elementConverter;
 84   
 85    /** Destination directory. */
 86    private File outputDirectory;
 87   
 88    /**
 89    * Constructor.
 90    *
 91    * @param prop QEDEQ module properties object.
 92    */
 93  0 public Qedeq2Wiki(final ModuleProperties prop) {
 94  0 this.prop = prop;
 95  0 this.elementConverter = new Element2Latex((prop.hasLoadedRequiredModules()
 96    ? prop.getRequiredModules() : null));
 97    }
 98   
 99    /**
 100    * Prints a LaTeX file into a given output stream.
 101    *
 102    * @param language Filter text to get and produce text in this language only.
 103    * @param level Filter for this detail level. TODO mime 20050205: not supported yet.
 104    * @param outputDirectory Write files to this directory.
 105    * @throws IOException
 106    */
 107  0 public final synchronized void printWiki(final String language, final String level,
 108    final File outputDirectory) throws IOException {
 109  0 if (language == null) {
 110  0 this.language = "en";
 111    } else {
 112  0 this.language = language;
 113    }
 114  0 this.outputDirectory = outputDirectory;
 115  0 printQedeqChapters();
 116  0 printQedeqBibliography();
 117  0 if (printer.checkError()) {
 118  0 throw new IOException("TODO mime: better use another OutputStream");
 119    }
 120    }
 121   
 122    /**
 123    * Print all chapters.
 124    *
 125    * @throws IOException Writing failed.
 126    */
 127  0 private void printQedeqChapters() throws IOException {
 128  0 final ChapterList chapters = prop.getModule().getQedeq().getChapterList();
 129  0 for (int i = 0; i < chapters.size(); i++) {
 130  0 final String label = prop.getModule().getQedeq().getHeader().getSpecification()
 131    .getName() + "_ch_" + i;
 132  0 final OutputStream outputStream = new FileOutputStream(new File(outputDirectory,
 133    label + "_" + language + ".wiki"));
 134  0 this.printer = new PrintStream(outputStream);
 135  0 final Chapter chapter = chapters.get(i);
 136  0 printer.print("\\chapter");
 137  0 if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) {
 138  0 printer.print("*");
 139    }
 140  0 printer.println("== " + getLatexListEntry(chapter.getTitle()) + " ==");
 141  0 printer.println();
 142  0 printer.println("<div id=\"" + label + "\"></div>");
 143    // if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) {
 144  0 printer.println();
 145  0 if (chapter.getIntroduction() != null) {
 146  0 printer.println(getLatexListEntry(chapter.getIntroduction()));
 147  0 printer.println();
 148    }
 149  0 final SectionList sections = chapter.getSectionList();
 150  0 if (sections != null) {
 151  0 printSections(i, sections);
 152  0 printer.println();
 153    }
 154  0 printer.println("%% end of chapter " + getLatexListEntry(chapter.getTitle()));
 155  0 printer.println();
 156    }
 157    }
 158   
 159    /**
 160    * Print bibliography (if any).
 161    */
 162  0 private void printQedeqBibliography() {
 163  0 final LiteratureItemList items = prop.getModule().getQedeq().getLiteratureItemList();
 164  0 if (items == null) {
 165  0 return;
 166    }
 167  0 printer.println("\\begin{thebibliography}{99}");
 168  0 for (int i = 0; i < items.size(); i++) {
 169  0 final LiteratureItem item = items.get(i);
 170  0 printer.print("\\bibitem{" + item.getLabel() + "} ");
 171  0 printer.println(getLatexListEntry(item.getItem()));
 172  0 printer.println();
 173    }
 174  0 printer.println("\\end{thebibliography}");
 175  0 printer.println("\\addcontentsline{toc}{chapter}{Literaturverzeichnis}");
 176    }
 177   
 178    /**
 179    * Print all given sections.
 180    *
 181    * @param chapter Chapter number.
 182    * @param sections List of sections.
 183    */
 184  0 private void printSections(final int chapter, final SectionList sections) {
 185  0 if (sections == null) {
 186  0 return;
 187    }
 188  0 for (int i = 0; i < sections.size(); i++) {
 189  0 final Section section = sections.get(i);
 190  0 printer.print("\\section{");
 191  0 printer.print(getLatexListEntry(section.getTitle()));
 192  0 final String label = "chapter" + chapter + "_section" + i;
 193  0 printer.println("} \\label{" + label + "} \\hypertarget{" + label + "}{}");
 194  0 printer.println(getLatexListEntry(section.getIntroduction()));
 195  0 printer.println();
 196  0 printSubsections(section.getSubsectionList());
 197    }
 198    }
 199   
 200    /**
 201    * Print all given subsections.
 202    *
 203    * @param nodes List of subsections.
 204    */
 205  0 private void printSubsections(final SubsectionList nodes) {
 206  0 if (nodes == null) {
 207  0 return;
 208    }
 209  0 for (int i = 0; i < nodes.size(); i++) {
 210  0 final SubsectionType subsectionType = nodes.get(i);
 211  0 if (subsectionType instanceof Node) {
 212  0 final Node node = (Node) subsectionType;
 213  0 printer.println(getLatexListEntry(node.getPrecedingText()));
 214  0 printer.println();
 215  0 printer.println("\\par");
 216  0 final String id = node.getId();
 217  0 final NodeType type = node.getNodeType();
 218  0 String title = null;
 219  0 if (node.getTitle() != null) {
 220  0 title = getLatexListEntry(node.getTitle());
 221    }
 222  0 if (type instanceof Axiom) {
 223  0 printAxiom((Axiom) type, title, id);
 224  0 } else if (type instanceof PredicateDefinition) {
 225  0 printPredicateDefinition((PredicateDefinition) type, title, id);
 226  0 } else if (type instanceof FunctionDefinition) {
 227  0 printFunctionDefinition((FunctionDefinition) type, title, id);
 228  0 } else if (type instanceof Proposition) {
 229  0 printProposition((Proposition) type, title, id);
 230  0 } else if (type instanceof Rule) {
 231  0 printRule((Rule) type, title, id);
 232    } else {
 233  0 throw new RuntimeException((type != null ? "unknown type: "
 234    + type.getClass().getName() : "node type empty"));
 235    }
 236  0 printer.println();
 237  0 printer.println(getLatexListEntry(node.getSucceedingText()));
 238    } else {
 239  0 final Subsection subsection = (Subsection) subsectionType;
 240  0 if (subsection.getTitle() != null) {
 241  0 printer.print("\\subsection{");
 242  0 printer.println(getLatexListEntry(subsection.getTitle()));
 243  0 printer.println("}");
 244    }
 245  0 printer.println(getLatexListEntry(subsection.getLatex()));
 246    }
 247  0 printer.println();
 248  0 printer.println();
 249    }
 250    }
 251   
 252    /**
 253    * Print axiom.
 254    *
 255    * @param axiom Print this.
 256    * @param title Extra name.
 257    * @param id Label for marking this axiom.
 258    */
 259  0 private void printAxiom(final Axiom axiom, final String title, final String id) {
 260  0 printer.println("\\begin{ax}" + (title != null ? "[" + title + "]" : ""));
 261  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 262  0 printFormula(axiom.getFormula().getElement());
 263  0 printer.println(getLatexListEntry(axiom.getDescription()));
 264  0 printer.println("\\end{ax}");
 265    }
 266   
 267    /**
 268    * Print top level formula. If the formula has the form <code>AND(.., .., ..)</code> the
 269    * formula is broken down in several labeled lines.
 270    *
 271    * @param element Formula to print.
 272    * @param mainLabel Main formula label.
 273    */
 274  0 private void printTopFormula(final Element element, final String mainLabel) {
 275  0 if (!element.isList() || !element.getList().getOperator().equals("AND")) {
 276  0 printFormula(element);
 277  0 return;
 278    }
 279  0 final ElementList list = element.getList();
 280  0 printer.println("\\mbox{}");
 281  0 printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{0.9\\linewidth}l}}");
 282  0 for (int i = 0; i < list.size(); i++) {
 283  0 final String label = (i < ALPHABET.length() ? "" + ALPHABET .charAt(i) : "" + i);
 284  0 printer.println("\\centering $" + getLatex(list.getElement(i)) + "$"
 285    + " & \\label{" + mainLabel + ":" + label + "} \\hypertarget{" + mainLabel + ":"
 286    + label + "}{} \\mbox{\\emph{(" + label + ")}} "
 287  0 + (i + 1 < list.size() ? "\\\\" : ""));
 288    }
 289  0 printer.println("\\end{longtable}");
 290    }
 291   
 292    /**
 293    * Print formula.
 294    *
 295    * @param element Formula to print.
 296    */
 297  0 private void printFormula(final Element element) {
 298  0 printer.println("\\mbox{}");
 299  0 printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{\\linewidth}}}");
 300  0 printer.println("\\centering $" + getLatex(element) + "$");
 301  0 printer.println("\\end{longtable}");
 302    }
 303   
 304    /**
 305    * Print predicate definition.
 306    *
 307    * @param definition Print this.
 308    * @param title Extra name.
 309    * @param id Label for marking this definition.
 310    */
 311  0 private void printPredicateDefinition(final PredicateDefinition definition, final String title,
 312    final String id) {
 313  0 final StringBuffer define = new StringBuffer("$$" + definition.getLatexPattern());
 314  0 final VariableList list = definition.getVariableList();
 315  0 if (list != null) {
 316  0 for (int i = list.size() - 1; i >= 0; i--) {
 317  0 Trace.trace(CLASS, this, "printDefinition", "replacing!");
 318  0 ReplaceUtility.replace(define, "#" + (i + 1), getLatex(list.get(i)));
 319    }
 320    }
 321  0 if (definition.getFormula() != null) {
 322  0 printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : ""));
 323  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 324  0 define.append("\\ :\\leftrightarrow \\ ");
 325  0 define.append(getLatex(definition.getFormula().getElement()));
 326    } else {
 327  0 printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : ""));
 328  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 329    }
 330  0 define.append("$$");
 331  0 elementConverter.addPredicate(definition);
 332  0 Trace.param(CLASS, this, "printDefinition", "define", define);
 333  0 printer.println(define);
 334  0 printer.println(getLatexListEntry(definition.getDescription()));
 335  0 if (definition.getFormula() != null) {
 336  0 printer.println("\\end{defn}");
 337    } else {
 338  0 printer.println("\\end{idefn}");
 339    }
 340    }
 341   
 342    /**
 343    * Print function definition.
 344    *
 345    * @param definition Print this.
 346    * @param title Extra name.
 347    * @param id Label for marking this definition.
 348    */
 349  0 private void printFunctionDefinition(final FunctionDefinition definition, final String title,
 350    final String id) {
 351  0 final StringBuffer define = new StringBuffer("$$" + definition.getLatexPattern());
 352  0 final VariableList list = definition.getVariableList();
 353  0 if (list != null) {
 354  0 for (int i = list.size() - 1; i >= 0; i--) {
 355  0 Trace.trace(CLASS, this, "printDefinition", "replacing!");
 356  0 ReplaceUtility.replace(define, "#" + (i + 1), getLatex(list.get(i)));
 357    }
 358    }
 359  0 if (definition.getTerm() != null) {
 360  0 printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : ""));
 361  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 362  0 define.append("\\ := \\ ");
 363  0 define.append(getLatex(definition.getTerm().getElement()));
 364    } else {
 365  0 printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : ""));
 366  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 367    }
 368  0 define.append("$$");
 369  0 elementConverter.addFunction(definition);
 370  0 Trace.param(CLASS, this, "printDefinition", "define", define);
 371  0 printer.println(define);
 372  0 printer.println(getLatexListEntry(definition.getDescription()));
 373  0 if (definition.getTerm() != null) {
 374  0 printer.println("\\end{defn}");
 375    } else {
 376  0 printer.println("\\end{idefn}");
 377    }
 378    }
 379   
 380    /**
 381    * Print proposition.
 382    *
 383    * @param proposition Print this.
 384    * @param title Extra name.
 385    * @param id Label for marking this proposition.
 386    */
 387  0 private void printProposition(final Proposition proposition, final String title,
 388    final String id) {
 389  0 printer.println("\\begin{prop}" + (title != null ? "[" + title + "]" : ""));
 390  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 391  0 printTopFormula(proposition.getFormula().getElement(), id);
 392  0 printer.println(getLatexListEntry(proposition.getDescription()));
 393  0 printer.println("\\end{prop}");
 394  0 if (proposition.getProofList() != null) {
 395  0 for (int i = 0; i < proposition.getProofList().size(); i++) {
 396  0 printer.println("\\begin{proof}");
 397  0 printer.println(getLatexListEntry(proposition.getProofList().get(i)
 398    .getNonFormalProof()));
 399  0 printer.println("\\end{proof}");
 400    }
 401    }
 402    }
 403   
 404    /**
 405    * Print rule declaration.
 406    *
 407    * @param rule Print this.
 408    * @param title Extra name.
 409    * @param id Label for marking this proposition.
 410    */
 411  0 private void printRule(final Rule rule, final String title,
 412    final String id) {
 413  0 printer.println("\\begin{rul}" + (title != null ? "[" + title + "]" : ""));
 414  0 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
 415  0 printer.println(getLatexListEntry(rule.getDescription()));
 416  0 printer.println("\\end{rul}");
 417   
 418    // TODO mime 20051210: are these informations equivalent to a formal proof?
 419    /*
 420    if (null != rule.getLinkList()) {
 421    printer.println("\\begin{proof}");
 422    printer.println("Rule name: " + rule.getName());
 423    printer.println();
 424    printer.println();
 425    for (int i = 0; i < rule.getLinkList().size(); i++) {
 426    printer.println(rule.getLinkList().get(i));
 427    }
 428    printer.println("\\end{proof}");
 429    }
 430    */
 431  0 if (rule.getProofList() != null) {
 432  0 for (int i = 0; i < rule.getProofList().size(); i++) {
 433  0 printer.println("\\begin{proof}");
 434  0 printer.println(getLatexListEntry(rule.getProofList().get(i)
 435    .getNonFormalProof()));
 436  0 printer.println("\\end{proof}");
 437    }
 438    }
 439    }
 440   
 441    /**
 442    * Get LaTeX element presentation.
 443    *
 444    * @param element Print this element.
 445    * @return LaTeX form of element.
 446    */
 447  0 private String getLatex(final Element element) {
 448  0 return elementConverter.getLatex(element);
 449    }
 450   
 451    /**
 452    * Filters correct entry out of LaTeX list. Filter criterion is for example the correct
 453    * language.
 454    * TODO mime 20050205: filter level too?
 455    *
 456    * @param list List of LaTeX texts.
 457    * @return Filtered text.
 458    */
 459  0 private String getLatexListEntry(final LatexList list) {
 460  0 if (list == null) {
 461  0 return "";
 462    }
 463  0 for (int i = 0; i < list.size(); i++) {
 464  0 if (language.equals(list.get(i).getLanguage())) {
 465  0 return getLatex(list.get(i));
 466    }
 467    }
 468    // assume entry with missing language as default
 469  0 for (int i = 0; i < list.size(); i++) {
 470  0 if (list.get(i).getLanguage() == null) {
 471  0 return getLatex(list.get(i));
 472    }
 473    }
 474  0 for (int i = 0; i < list.size(); i++) { // LATER mime 20050222: evaluate default?
 475  0 return "MISSING! OTHER: " + getLatex(list.get(i));
 476    }
 477  0 return "MISSING!";
 478    }
 479   
 480    /**
 481    * Get really LaTeX. Does some simple character replacements for umlauts.
 482    * TODO mime 20050205: filter more than German umlauts
 483    *
 484    * @param latex Unescaped text.
 485    * @return Really LaTeX.
 486    */
 487  0 private String getLatex(final Latex latex) {
 488  0 if (latex == null || latex.getLatex() == null) {
 489  0 return "";
 490    }
 491  0 return LatexTextParser.transform(latex.getLatex());
 492    }
 493   
 494    }
 
CloverReport generated by Clover Code Coverage v1.3.10
Sa Jan 26 2008 15:40:52 CET.		   Open Source License registered to the Hilbert II Project. This license of Clover is provided to support the development of Hilbert II only.