Clover coverage report - QedeqKernelSe Coverage Report
Coverage timestamp: Do Dez 29 2005 18:38:29 CET
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 756   Methods: 20
NCLOC: 546   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
Qedeq2Latex.java 74,7% 83,6% 100% 81,6%
coverage coverage
 1    /* $Id: Qedeq2Latex.java,v 1.40 2005/12/29 17:31:10 m31 Exp $
 2    *
 3    * This file is part of the project "Hilbert II" - http://www.qedeq.org
 4    *
 5    * Copyright 2000-2005, 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.elli.Element;
 29    import org.qedeq.kernel.base.elli.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.Definition;
 36    import org.qedeq.kernel.base.module.Latex;
 37    import org.qedeq.kernel.base.module.LatexList;
 38    import org.qedeq.kernel.base.module.Node;
 39    import org.qedeq.kernel.base.module.NodeType;
 40    import org.qedeq.kernel.base.module.Proposition;
 41    import org.qedeq.kernel.base.module.Qedeq;
 42    import org.qedeq.kernel.base.module.Rule;
 43    import org.qedeq.kernel.base.module.Section;
 44    import org.qedeq.kernel.base.module.SectionList;
 45    import org.qedeq.kernel.base.module.Subsection;
 46    import org.qedeq.kernel.base.module.SubsectionList;
 47    import org.qedeq.kernel.base.module.SubsectionType;
 48    import org.qedeq.kernel.base.module.VariableList;
 49    import org.qedeq.kernel.bo.control.IllegalModuleDataException;
 50    import org.qedeq.kernel.bo.control.QedeqBoFactory;
 51    import org.qedeq.kernel.dto.module.DefinitionVo;
 52    import org.qedeq.kernel.log.Trace;
 53    import org.qedeq.kernel.utility.ReplaceUtility;
 54   
 55   
 56    /**
 57    * Transfer a qedeq module into a LaTeX file.
 58    * <p>
 59    * <b>TODO mime 20050205: This is just a quick hacked generator. No parsing or validation
 60    * of inline LaTeX text is done. No reference is resolved. This class just
 61    * generates some LaTeX to get some visual impression of a qedeq module
 62    * in an early development stage.</b>
 63    *
 64    * @version $Revision: 1.40 $
 65    * @author Michael Meyling
 66    */
 67    public final class Qedeq2Latex {
 68   
 69    /** Output goes here. */
 70    private PrintStream printer;
 71   
 72    /** Qedeq module to transfer into LaTeX form. */
 73    private Qedeq qedeq;
 74   
 75    /** Filter text to get and produce text in this language. */
 76    private String language;
 77   
 78    /** Filter for this detail level. TODO mime 20050205: not used yet. */
 79    private Object level;
 80   
 81    /** Maps identifiers to {@link Definition}s. */
 82    private Map definitions = new HashMap();
 83   
 84    /**
 85    * Constructor.
 86    *
 87    * @param context Context within this module is created.
 88    * @param qedeq Work with this qedeq module.
 89    * @throws IllegalModuleDataException
 90    */
 91  7 public Qedeq2Latex(final String context, final Qedeq qedeq) throws IllegalModuleDataException {
 92  7 this.qedeq = QedeqBoFactory.createQedeq(context, qedeq);
 93  6 final DefinitionVo definition = new DefinitionVo();
 94    // TODO mime 20050224: quick hack to have the logical identity operator
 95  6 definition.setArgumentNumber("2");
 96  6 definition.setType("PREDCON");
 97  6 definition.setLatexPattern("#1 \\ = \\ #2");
 98  6 definitions.put("equal", definition);
 99    }
 100   
 101    /**
 102    * Prints a LaTeX file into a given output stream.
 103    *
 104    * @param language Filter text to get and produce text in this language only.
 105    * @param level Filter for this detail level. TODO mime 20050205: not supported yet.
 106    * @param outputStream Write output herein.
 107    * @throws IOException
 108    */
 109  6 public final synchronized void printLatex(final String language, final String level,
 110    final OutputStream outputStream) throws IOException {
 111  6 if (language == null) {
 112  0 this.language = "en";
 113    } else {
 114  6 this.language = language;
 115    }
 116  6 if (level == null) {
 117  0 this.level = "1";
 118    } else {
 119  6 this.level = level;
 120    }
 121  6 this.printer = new PrintStream(outputStream);
 122  6 printLatexHeader();
 123  6 printQedeqHeader();
 124  6 printQedeqChapters();
 125  6 printLatexTrailer();
 126  6 if (printer.checkError()) {
 127  0 throw new IOException("TODO mime: better use another OutputStream");
 128    }
 129    }
 130   
 131    /**
 132    * Prints the header.
 133    */
 134  6 private void printQedeqHeader() {
 135  6 final LatexList title = qedeq.getHeader().getTitle();
 136  6 printer.print("\\title{");
 137  6 printer.print(getLatexListEntry(title));
 138  6 printer.println("}");
 139  6 printer.println("\\author{");
 140  6 final AuthorList authors = qedeq.getHeader().getAuthorList();
 141  6 for (int i = 0; i < authors.size(); i++) {
 142  6 final Author author = authors.get(i);
 143  6 printer.println(author.getName().getLatex());
 144    }
 145  6 printer.println("}");
 146  6 printer.println();
 147  6 printer.println("\\begin{document}");
 148  6 printer.println();
 149  6 printer.println("\\maketitle");
 150  6 printer.println();
 151  6 printer.println("\\setlength{\\parskip}{0pt}");
 152  6 printer.println("\\tableofcontents");
 153  6 printer.println("\\setlength{\\parskip}{5pt plus 2pt minus 1pt}");
 154  6 printer.println();
 155    }
 156   
 157    /**
 158    * Print all chapters.
 159    */
 160  6 private void printQedeqChapters() {
 161  6 final ChapterList chapters = qedeq.getChapterList();
 162  6 for (int i = 0; i < chapters.size(); i++) {
 163  22 final Chapter chapter = chapters.get(i);
 164  22 printer.print("\\chapter");
 165  22 if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) {
 166  8 printer.print("*");
 167    }
 168  22 printer.print("{");
 169  22 printer.print(getLatexListEntry(chapter.getTitle()));
 170  22 printer.println("} \\label{" + "chapter" + i + "}");
 171  22 if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) {
 172  8 printer.println("\\addcontentsline{toc}{chapter}{"
 173    + getLatexListEntry(chapter.getTitle()) + "}");
 174    }
 175  22 printer.println();
 176  22 if (chapter.getIntroduction() != null) {
 177  22 printer.println(getLatexListEntry(chapter.getIntroduction()));
 178  22 printer.println();
 179    }
 180  22 final SectionList sections = chapter.getSectionList();
 181  22 if (sections != null) {
 182  10 printSections(sections);
 183  10 printer.println();
 184    }
 185  22 printer.println("%% end of chapter " + getLatexListEntry(chapter.getTitle()));
 186  22 printer.println();
 187    }
 188    }
 189   
 190    /**
 191    * Print all given sections.
 192    *
 193    * @param sections List of sections.
 194    */
 195  10 private void printSections(final SectionList sections) {
 196  10 if (sections == null) {
 197  0 return;
 198    }
 199  10 for (int i = 0; i < sections.size(); i++) {
 200  20 final Section section = sections.get(i);
 201  20 printer.print("\\section{");
 202  20 printer.print(getLatexListEntry(section.getTitle()));
 203  20 printer.println("} \\label{" + "section" + i + "}");
 204  20 printer.println(getLatexListEntry(section.getIntroduction()));
 205  20 printer.println();
 206  20 printSubsections(section.getSubsectionList());
 207    }
 208    }
 209   
 210    /**
 211    * Print all given subsections.
 212    *
 213    * @param nodes List of subsections.
 214    */
 215  20 private void printSubsections(final SubsectionList nodes) {
 216  20 if (nodes == null) {
 217  12 return;
 218    }
 219  8 for (int i = 0; i < nodes.size(); i++) {
 220  48 final SubsectionType subsectionType = nodes.get(i);
 221  48 if (subsectionType instanceof Node) {
 222  28 final Node node = (Node) subsectionType;
 223  28 printer.println(getLatexListEntry(node.getPrecedingText()));
 224  28 printer.println();
 225  28 printer.println("\\par");
 226  28 final String id = node.getId();
 227  28 final NodeType type = node.getNodeType();
 228  28 String title = null;
 229  28 if (node.getTitle() != null) {
 230  18 title = getLatexListEntry(node.getTitle());
 231    }
 232  28 if (type instanceof Axiom) {
 233  6 printAxiom((Axiom) type, title, id);
 234  22 } else if (type instanceof Definition) {
 235  10 printDefinition((Definition) type, title, id);
 236  12 } else if (type instanceof Proposition) {
 237  10 printProposition((Proposition) type, title, id);
 238  2 } else if (type instanceof Rule) {
 239  2 printRule((Rule) type, title, id);
 240    } else {
 241  0 throw new RuntimeException((type != null ? "unknown type: "
 242    + type.getClass().getName() : "node type empty"));
 243    }
 244  28 printer.println();
 245  28 printer.println(getLatexListEntry(node.getSucceedingText()));
 246    } else {
 247  20 printer.print("\\subsection{");
 248  20 final Subsection subsection = (Subsection) subsectionType;
 249  20 printer.println(getLatexListEntry(subsection.getTitle()));
 250  20 printer.println("}");
 251  20 printer.println(getLatexListEntry(subsection.getLatex()));
 252    }
 253  48 printer.println();
 254  48 printer.println();
 255    }
 256    }
 257   
 258    /**
 259    * Print axiom.
 260    *
 261    * @param axiom Print this.
 262    * @param title Extra name.
 263    * @param id Label for marking this axiom.
 264    */
 265  6 private void printAxiom(final Axiom axiom, final String title, final String id) {
 266  6 printer.println("\\begin{ax}" + (title != null ? "[" + title + "]" : ""));
 267  6 printer.println("\\label{" + id + "}");
 268  6 printFormula(axiom.getFormula().getElement());
 269  6 printer.println(getLatexListEntry(axiom.getDescription()));
 270  6 printer.println("\\end{ax}");
 271    }
 272   
 273    /**
 274    * Print formula.
 275    *
 276    * @param element Formula to print.
 277    */
 278  16 private void printFormula(final Element element) {
 279  16 printer.println("\\mbox{}");
 280  16 printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{\\linewidth}}}");
 281  16 printer.println("$" + getLatex(element) + "$");
 282  16 printer.println("\\end{longtable}");
 283    }
 284   
 285    /**
 286    * Print definition.
 287    *
 288    * @param definition Print this.
 289    * @param title Extra name.
 290    * @param id Label for marking this definition.
 291    */
 292  10 private void printDefinition(final Definition definition, final String title,
 293    final String id) {
 294  10 final StringBuffer define = new StringBuffer("$$" + definition.getLatexPattern());
 295  10 final VariableList list = definition.getVariableList();
 296  10 if (list != null) {
 297  10 for (int i = list.size() - 1; i >= 0; i--) {
 298  16 Trace.trace(this, "printDefinition", "replacing!");
 299  16 ReplaceUtility.replace(define, "#" + (i + 1), getLatex(list.get(i)));
 300    }
 301    }
 302  10 if (definition.getFormulaOrTerm() != null) {
 303  6 printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : ""));
 304  6 printer.println("\\label{" + id + "}");
 305  6 define.append("\\ := \\ ");
 306  6 define.append(getLatex(definition.getFormulaOrTerm().getElement()));
 307    } else {
 308  4 printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : ""));
 309  4 printer.println("\\label{" + id + "}");
 310    }
 311  10 define.append("$$");
 312  10 definitions.put(id, definition);
 313  10 Trace.traceParam(this, "printDefinition", "define", define);
 314  10 printer.println(define);
 315  10 printer.println(getLatexListEntry(definition.getDescription()));
 316  10 if (definition.getFormulaOrTerm() != null) {
 317  6 printer.println("\\end{defn}");
 318    } else {
 319  4 printer.println("\\end{idefn}");
 320    }
 321    }
 322   
 323    /**
 324    * Print proposition.
 325    *
 326    * @param proposition Print this.
 327    * @param title Extra name.
 328    * @param id Label for marking this proposition.
 329    */
 330  10 private void printProposition(final Proposition proposition, final String title,
 331    final String id) {
 332  10 printer.println("\\begin{prop}" + (title != null ? "[" + title + "]" : ""));
 333  10 printer.println("\\label{" + id + "}");
 334  10 printFormula(proposition.getFormula().getElement());
 335  10 printer.println(getLatexListEntry(proposition.getDescription()));
 336  10 printer.println("\\end{prop}");
 337  10 if (proposition.getProofList() != null) {
 338  10 for (int i = 0; i < proposition.getProofList().size(); i++) {
 339  10 printer.println("\\begin{proof}");
 340  10 printer.println(getLatexListEntry(proposition.getProofList().get(i)
 341    .getNonFormalProof()));
 342  10 printer.println("\\end{proof}");
 343    }
 344    }
 345    }
 346   
 347    /**
 348    * Print rule declaration.
 349    *
 350    * @param rule Print this.
 351    * @param title Extra name.
 352    * @param id Label for marking this proposition.
 353    */
 354  2 private void printRule(final Rule rule, final String title,
 355    final String id) {
 356  2 printer.println("\\begin{rul}" + (title != null ? "[" + title + "]" : ""));
 357  2 printer.println("\\label{" + id + "}");
 358  2 printer.println(getLatexListEntry(rule.getDescription()));
 359  2 printer.println("\\end{rul}");
 360   
 361    // TODO mime 20051210: are these informations equivalent to a formal proof?
 362    /*
 363    if (null != rule.getLinkList()) {
 364    printer.println("\\begin{proof}");
 365    printer.println("Rule name: " + rule.getName());
 366    printer.println();
 367    printer.println();
 368    for (int i = 0; i < rule.getLinkList().size(); i++) {
 369    printer.println(rule.getLinkList().get(i));
 370    }
 371    printer.println("\\end{proof}");
 372    }
 373    */
 374  2 if (rule.getProofList() != null) {
 375  0 for (int i = 0; i < rule.getProofList().size(); i++) {
 376  0 printer.println("\\begin{proof}");
 377  0 printer.println(getLatexListEntry(rule.getProofList().get(i)
 378    .getNonFormalProof()));
 379  0 printer.println("\\end{proof}");
 380    }
 381    }
 382    }
 383   
 384    /**
 385    * Get LaTeX element presentation.
 386    *
 387    * @param element Print this element.
 388    * @return LaTeX form of element.
 389    */
 390  38 private String getLatex(final Element element) {
 391  38 return getLatex(element, true);
 392    }
 393   
 394    /**
 395    * Get LaTeX element presentation.
 396    *
 397    * @param element Print this element.
 398    * @param first First level?
 399    * @return LaTeX form of element.
 400    */
 401  444 private String getLatex(final Element element, final boolean first) {
 402  444 final StringBuffer buffer = new StringBuffer();
 403  444 if (element.isAtom()) {
 404  0 return element.getAtom().getString();
 405    }
 406  444 final ElementList list = element.getList();
 407  444 if (list.getOperator().equals("PREDCON")) {
 408  78 final String identifier = list.getElement(0).getAtom().getString();
 409  78 if (definitions.containsKey(identifier)) {
 410  78 final Definition definition = (Definition) definitions.get(identifier);
 411  78 final StringBuffer define = new StringBuffer(definition.getLatexPattern());
 412  78 for (int i = list.size() - 1; i >= 1; i--) {
 413  146 ReplaceUtility.replace(define, "#" + i, getLatex(list.getElement(i), false));
 414    }
 415  78 buffer.append(define);
 416    } else {
 417  0 buffer.append(identifier);
 418  0 buffer.append("(");
 419  0 for (int i = 1; i < list.size(); i++) {
 420  0 buffer.append(getLatex(list.getElement(i), false));
 421  0 if (i + 1 < list.size()) {
 422  0 buffer.append(", ");
 423    }
 424    }
 425  0 buffer.append(")");
 426    }
 427  366 } else if (list.getOperator().equals("PREDVAR")) {
 428  32 final String identifier = list.getElement(0).getAtom().getString();
 429  32 buffer.append(identifier);
 430  32 buffer.append("(");
 431  32 for (int i = 1; i < list.size(); i++) {
 432  32 buffer.append(getLatex(list.getElement(i), false));
 433  32 if (i + 1 < list.size()) {
 434  0 buffer.append(", ");
 435    }
 436    }
 437  32 buffer.append(")");
 438  334 } else if (list.getOperator().equals("VAR")) {
 439  222 final String text = list.getElement(0).getAtom().getString();
 440  222 try {
 441  222 final int index = Integer.parseInt(text);
 442  0 switch (index) {
 443  0 case 1:
 444  0 return "x";
 445  0 case 2:
 446  0 return "y";
 447  0 case 3:
 448  0 return "z";
 449  0 case 4:
 450  0 return "u";
 451  0 case 5:
 452  0 return "v";
 453  0 case 6:
 454  0 return "w";
 455  0 default:
 456  0 return "x_" + (index - 6);
 457    }
 458    } catch (NumberFormatException e) {
 459  222 return text;
 460    }
 461  112 } else if (list.getOperator().equals("AND") || list.getOperator().equals("OR")
 462    || list.getOperator().equals("EQUI") || list.getOperator().equals("IMPL")) {
 463  52 final String infix;
 464  52 if (list.getOperator().equals("AND")) {
 465  10 infix = "\\ \\land \\ ";
 466  42 } else if (list.getOperator().equals("OR")) {
 467  0 infix = "\\ \\lor \\ ";
 468  42 } else if (list.getOperator().equals("EQUI")) {
 469  30 infix = "\\ \\leftrightarrow \\ ";
 470    } else {
 471  12 infix = "\\ \\rightarrow \\ ";
 472    }
 473  52 if (!first) {
 474  40 buffer.append("(");
 475    }
 476  52 for (int i = 0; i < list.size(); i++) {
 477  110 buffer.append(getLatex(list.getElement(i), false));
 478  110 if (i + 1 < list.size()) {
 479  58 buffer.append(infix);
 480    }
 481    }
 482  52 if (!first) {
 483  40 buffer.append(")");
 484    }
 485  60 } else if (list.getOperator().equals("FORALL") || list.getOperator().equals("EXISTS")
 486    || list.getOperator().equals("EXISTSU")) {
 487  32 final String prefix;
 488  32 if (list.getOperator().equals("FORALL")) {
 489  24 prefix = "\\forall ";
 490  8 } else if (list.getOperator().equals("EXISTS")) {
 491  6 prefix = "\\exists ";
 492    } else {
 493  2 prefix = "\\exists! ";
 494    }
 495  32 buffer.append(prefix);
 496  32 for (int i = 0; i < list.size(); i++) {
 497  68 if (i != 0 || (i == 0 && list.size() <= 2)) {
 498  64 buffer.append(getLatex(list.getElement(i), false));
 499    }
 500  68 if (i + 1 < list.size()) {
 501  36 buffer.append("\\ ");
 502    }
 503    }
 504  28 } else if (list.getOperator().equals("NOT")) {
 505  2 final String prefix = "\\neg ";
 506  2 buffer.append(prefix);
 507  2 for (int i = 0; i < list.size(); i++) {
 508  2 buffer.append(getLatex(list.getElement(i), false));
 509    }
 510  26 } else if (list.getOperator().equals("SET")) {
 511  26 final String prefix = "\\{ ";
 512  26 buffer.append(prefix);
 513  26 for (int i = 0; i < list.size(); i++) {
 514  52 buffer.append(getLatex(list.getElement(i), false));
 515  52 if (i + 1 < list.size()) {
 516  26 buffer.append(" \\ | \\ ");
 517    }
 518    }
 519  26 buffer.append(" \\} ");
 520    } else {
 521  0 buffer.append(list.getOperator());
 522  0 buffer.append("(");
 523  0 for (int i = 0; i < list.size(); i++) {
 524  0 buffer.append(getLatex(list.getElement(i), false));
 525  0 if (i + 1 < list.size()) {
 526  0 buffer.append(", ");
 527    }
 528    }
 529  0 buffer.append(")");
 530    }
 531  222 return buffer.toString();
 532    }
 533   
 534    /**
 535    * Print LaTeX lines for the file head.
 536    */
 537  6 private void printLatexHeader() {
 538  6 printer.println("% -*- TeX:" + language.toUpperCase() + " -*-");
 539  6 printer.println("%%% ====================================================================");
 540  6 printer.println("%%% @LaTeX-file " + getFileName());
 541  6 printer.println("%%% Generated at " + getTimestamp());
 542  6 printer.println("%%% ====================================================================");
 543  6 printer.println();
 544  6 printer.println(
 545    "%%% Permission is granted to copy, distribute and/or modify this document");
 546  6 printer.println("%%% under the terms of the GNU Free Documentation License, Version 1.2");
 547  6 printer.println("%%% or any later version published by the Free Software Foundation;");
 548  6 printer.println(
 549    "%%% with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts.");
 550  6 printer.println();
 551  6 printer.println("\\documentclass[a4paper,german,10pt,twoside]{book}");
 552  6 if ("de".equals(language)) {
 553  3 printer.println("\\usepackage[german]{babel}");
 554  3 } else if ("en".equals(language)) {
 555  3 printer.println("\\usepackage[english]{babel}");
 556    } else {
 557  0 printer.println("%%% TODO unknown language: " + language);
 558  0 printer.println("%%% TODO using default language");
 559  0 printer.println("\\usepackage[english]{babel}");
 560    }
 561  6 printer.println("\\usepackage{makeidx}");
 562  6 printer.println("\\usepackage{amsmath,amsthm,amssymb}");
 563  6 printer.println("\\usepackage{color}");
 564  6 printer.println("\\usepackage[bookmarks,bookmarksnumbered,bookmarksopen,");
 565  6 printer.println(" colorlinks,linkcolor=webgreen,pagebackref]{hyperref}");
 566  6 printer.println("\\definecolor{webgreen}{rgb}{0,.5,0}");
 567  6 printer.println("\\usepackage{graphicx}");
 568  6 printer.println("\\usepackage{xr}");
 569  6 printer.println("\\usepackage{epsfig,longtable}");
 570  6 printer.println("\\usepackage{tabularx}");
 571  6 printer.println();
 572  6 if ("de".equals(language)) {
 573  3 printer.println("\\newtheorem{thm}{Theorem}[chapter]");
 574  3 printer.println("\\newtheorem{cor}[thm]{Korollar}");
 575  3 printer.println("\\newtheorem{lem}[thm]{Lemma}");
 576  3 printer.println("\\newtheorem{prop}[thm]{Proposition}");
 577  3 printer.println("\\newtheorem{ax}{Axiom}");
 578  3 printer.println("\\newtheorem{rul}{Regel}");
 579  3 printer.println();
 580  3 printer.println("\\theoremstyle{definition}");
 581  3 printer.println("\\newtheorem{defn}[thm]{Definition}");
 582  3 printer.println("\\newtheorem{idefn}[thm]{Initiale Definition}");
 583  3 printer.println();
 584  3 printer.println("\\theoremstyle{remark}");
 585  3 printer.println("\\newtheorem{rem}[thm]{Bemerkung}");
 586  3 printer.println("\\newtheorem*{notation}{Notation}");
 587  3 } else if ("en".equals(language)) {
 588  3 printer.println("\\newtheorem{thm}{Theorem}[chapter]");
 589  3 printer.println("\\newtheorem{cor}[thm]{Corollary}");
 590  3 printer.println("\\newtheorem{lem}[thm]{Lemma}");
 591  3 printer.println("\\newtheorem{prop}[thm]{Proposition}");
 592  3 printer.println("\\newtheorem{ax}{Axiom}");
 593  3 printer.println("\\newtheorem{rul}{Rule}");
 594  3 printer.println();
 595  3 printer.println("\\theoremstyle{definition}");
 596  3 printer.println("\\newtheorem{defn}[thm]{Definition}");
 597  3 printer.println("\\newtheorem{idefn}[thm]{Initial Definition}");
 598  3 printer.println();
 599  3 printer.println("\\theoremstyle{remark}");
 600  3 printer.println("\\newtheorem{rem}[thm]{Remark}");
 601  3 printer.println("\\newtheorem*{notation}{Notation}");
 602    } else {
 603  0 printer.println("%%% TODO unknown language: " + language);
 604  0 printer.println("%%% TODO using default language");
 605  0 printer.println("\\newtheorem{thm}{Theorem}[chapter]");
 606  0 printer.println("\\newtheorem{cor}[thm]{Corollary}");
 607  0 printer.println("\\newtheorem{lem}[thm]{Lemma}");
 608  0 printer.println("\\newtheorem{prop}[thm]{Proposition}");
 609  0 printer.println("\\newtheorem{ax}{Axiom}");
 610  0 printer.println();
 611  0 printer.println("\\theoremstyle{definition}");
 612  0 printer.println("\\newtheorem{defn}[thm]{Definition}");
 613  0 printer.println("\\newtheorem{idefn}[thm]{Initial Definition}");
 614  0 printer.println();
 615  0 printer.println("\\theoremstyle{remark}");
 616  0 printer.println("\\newtheorem{rem}[thm]{Remark}");
 617  0 printer.println("\\newtheorem*{notation}{Notation}");
 618    }
 619  6 printer.println();
 620  6 printer.println("\\addtolength{\\textheight}{7\\baselineskip}");
 621  6 printer.println("\\addtolength{\\topmargin}{-5\\baselineskip}");
 622  6 printer.println();
 623  6 printer.println("\\setlength{\\parindent}{0pt}");
 624  6 printer.println();
 625  6 printer.println("\\frenchspacing \\sloppy");
 626  6 printer.println();
 627  6 printer.println("\\makeindex");
 628  6 printer.println();
 629  6 printer.println();
 630    }
 631   
 632    /**
 633    * Print LaTeX trailer.
 634    */
 635  6 private void printLatexTrailer() {
 636  6 printer.println("\\backmatter");
 637  6 printer.println();
 638  6 printer.println("\\addcontentsline{toc}{chapter}{\\indexname} \\printindex");
 639  6 printer.println();
 640  6 printer.println("\\end{document}");
 641  6 printer.println();
 642    }
 643   
 644    /**
 645    * Get regular name for the LaTeX file.
 646    *
 647    * @return File name.
 648    */
 649  6 private String getFileName() {
 650    // FIXME mime 20050805: add language, validate with currently used file name e.g.
 651    // qedeq_basic_concept_en.tex
 652  6 return qedeq.getHeader().getSpecification().getName() + "_"
 653    + qedeq.getHeader().getSpecification().getRuleVersion() + ".tex";
 654    }
 655   
 656    /**
 657    * Get timestamp.
 658    *
 659    * @return Current timestamp.
 660    */
 661  6 private String getTimestamp() {
 662  6 final SimpleDateFormat formatter = new SimpleDateFormat("yyyy-MM-dd' 'HH:mm:ss,SSS");
 663  6 return formatter.format(new Date()).toString();
 664    }
 665   
 666    /**
 667    * Filters correct entry out of LaTeX list. Filter criterion is for example the correct
 668    * language.
 669    * TODO mime 20050205: filter level too?
 670    *
 671    * @param list List of LaTeX texts.
 672    * @return Filtered text.
 673    */
 674  272 private String getLatexListEntry(final LatexList list) {
 675  272 if (list == null) {
 676  36 return "";
 677    }
 678  236 for (int i = 0; i < list.size(); i++) {
 679  294 if (language.equals(list.get(i).getLanguage())) {
 680  116 return getLatex(list.get(i));
 681    }
 682    }
 683    // assume entry with missing language as default
 684  120 for (int i = 0; i < list.size(); i++) {
 685  120 if (list.get(i).getLanguage() == null) {
 686  120 return getLatex(list.get(i));
 687    }
 688    }
 689  0 for (int i = 0; i < list.size(); i++) { // TODO mime 20050222: evaluate default?
 690  0 return "MISSING! OTHER: " + getLatex(list.get(i));
 691    }
 692  0 return "MISSING!";
 693    }
 694   
 695    /**
 696    * Get really LaTeX. Does some simple character replacements for umlauts.
 697    * TODO mime 20050205: filter more than German umlauts
 698    *
 699    * @param latex Unescaped text.
 700    * @return Really LaTeX.
 701    */
 702  236 private String getLatex(final Latex latex) {
 703  236 final StringBuffer buffer = new StringBuffer(latex.getLatex());
 704  236 deleteLineLeadingWhitespace(buffer);
 705  236 ReplaceUtility.replace(buffer, "ü", "{\\\"u}");
 706  236 ReplaceUtility.replace(buffer, "ö", "{\\\"o}");
 707  236 ReplaceUtility.replace(buffer, "ä", "{\\\"a}");
 708  236 ReplaceUtility.replace(buffer, "Ü", "{\\\"U}");
 709  236 ReplaceUtility.replace(buffer, "Ö", "{\\\"O}");
 710  236 ReplaceUtility.replace(buffer, "Ä", "{\\\"A}");
 711  236 ReplaceUtility.replace(buffer, "ß", "{\\\"s}");
 712  236 return buffer.toString();
 713    }
 714   
 715    /**
 716    * Search for first line followed by whitespace and delete this string within the whole
 717    * text.
 718    * <p>
 719    * For example the following text
 720    *<pre>
 721    * Do you know the muffin man,
 722    * The muffin man, the muffin man,
 723    * Do you know the muffin man,
 724    * Who lives on Drury Lane?
 725    *</pre>
 726    * will be converted into:
 727    *<pre>
 728    *Do you know the muffin man,
 729    *The muffin man, the muffin man,
 730    *Do you know the muffin man,
 731    *Who lives on Drury Lane?
 732    *</pre>
 733    *
 734    * @param buffer Work on this text.
 735    */
 736  236 private void deleteLineLeadingWhitespace(final StringBuffer buffer) {
 737  236 int start = -1;
 738  ? while (0 <= (start = buffer.indexOf("\n", start + 1))) {
 739  73 if (start + 1 < buffer.length() && '\n' != buffer.charAt(start + 1)) {
 740  60 break;
 741    }
 742    }
 743  236 if (start >= 0) {
 744  60 int next = start + 1;
 745  60 while (next < buffer.length() && Character.isWhitespace(buffer.charAt(next))
 746    && '\n' != buffer.charAt(next)) {
 747  762 next++;
 748    }
 749  60 final String empty = buffer.substring(start, next);
 750  60 if (empty.length() > 0) {
 751  60 ReplaceUtility.replace(buffer, empty, "\n");
 752    }
 753    }
 754    }
 755   
 756    }
 
CloverReport generated by Clover Code Coverage v1.3.8
Do Dez 29 2005 18:39:59 CET.		   Open Source License registered to the Hilbert II Project. This license of Clover is provided to support the development of Hilbert II only.