Clover coverage report - QedeqKernelSe Coverage Report
Coverage timestamp: So Sep 2 2007 02:40:58 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.7 2007/08/21 21:03:30 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    * LATER 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.7 $
 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