/* $Id: Qedeq2Latex.java,v 1.41 2006/10/20 20:23:08 m31 Exp $
 *
 * This file is part of the project "Hilbert II" - http://www.qedeq.org
 *
 * Copyright 2000-2006,  Michael Meyling <mime@qedeq.org>.
 *
 * "Hilbert II" is free software; you can redistribute
 * it and/or modify it under the terms of the GNU General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 * GNU General Public License for more details.
 */

package org.qedeq.kernel.latex;

import java.io.IOException;
import java.io.OutputStream;
import java.io.PrintStream;
import java.text.SimpleDateFormat;
import java.util.Date;
import java.util.HashMap;
import java.util.Map;

import org.qedeq.kernel.base.list.Element;
import org.qedeq.kernel.base.list.ElementList;
import org.qedeq.kernel.base.module.Author;
import org.qedeq.kernel.base.module.AuthorList;
import org.qedeq.kernel.base.module.Axiom;
import org.qedeq.kernel.base.module.Chapter;
import org.qedeq.kernel.base.module.ChapterList;
import org.qedeq.kernel.base.module.FunctionDefinition;
import org.qedeq.kernel.base.module.Latex;
import org.qedeq.kernel.base.module.LatexList;
import org.qedeq.kernel.base.module.LiteratureItem;
import org.qedeq.kernel.base.module.LiteratureItemList;
import org.qedeq.kernel.base.module.Node;
import org.qedeq.kernel.base.module.NodeType;
import org.qedeq.kernel.base.module.PredicateDefinition;
import org.qedeq.kernel.base.module.Proposition;
import org.qedeq.kernel.base.module.Qedeq;
import org.qedeq.kernel.base.module.Rule;
import org.qedeq.kernel.base.module.Section;
import org.qedeq.kernel.base.module.SectionList;
import org.qedeq.kernel.base.module.Subsection;
import org.qedeq.kernel.base.module.SubsectionList;
import org.qedeq.kernel.base.module.SubsectionType;
import org.qedeq.kernel.base.module.VariableList;
import org.qedeq.kernel.bo.control.QedeqBoFactory;
import org.qedeq.kernel.bo.module.ModuleDataException;
import org.qedeq.kernel.dto.module.PredicateDefinitionVo;
import org.qedeq.kernel.log.Trace;
import org.qedeq.kernel.utility.IoUtility;
import org.qedeq.kernel.utility.ReplaceUtility;


/**
 * Transfer a qedeq module into a LaTeX file.
 * <p>
 * <b>TODO mime 20050205: This is just a quick hacked generator. No parsing or validation
 * of inline LaTeX text is done. No reference is resolved. This class just
 * generates some LaTeX to get some visual impression of a QEDEQ module
 * in an early development stage.</b>
 * <p>
 * This generator operates operates against the interface declaration of a QEDEQ module.
 * No business object is required.
 *
 * @version $Revision: 1.41 $
 * @author  Michael Meyling
 */
public final class Qedeq2Latex {

    /** Alphabet for tagging. */
    private static final String ALPHABET = "abcdefghijklmnopqrstuvwxyz";

    /** Output goes here. */
    private PrintStream printer;

    /** Qedeq module to transfer into LaTeX form. */
    private Qedeq qedeq;

    /** Filter text to get and produce text in this language. */
    private String language;

    /** Filter for this detail level. TODO mime 20050205: not used yet. */
    private Object level;

    /** Maps identifiers to {@link PredicateDefinition}s. */    // FIXME mime 20070102: also for Function Definitions!!!
    private Map definitions = new HashMap();

    /**
     * Constructor.
     *
     * @param   context Context within this module is created.
     * @param   qedeq   Work with this qedeq module.
     * @throws  ModuleDataException
     */
    public Qedeq2Latex(final String context, final Qedeq qedeq) throws ModuleDataException {
        // although we work against the interfaces we create an BO just for testing purposes
        this.qedeq = QedeqBoFactory.createQedeq(context, qedeq);
        final PredicateDefinitionVo equal = new PredicateDefinitionVo();
        // TODO mime 20050224: quick hack to have the logical identity operator
        equal.setArgumentNumber("2");
        equal.setName("equal");
        equal.setLatexPattern("#1 \\ =  \\ #2");
        definitions.put("equal_2", equal);
        // TODO mime 20060822: quick hack to get the negation of the logical identity operator
        final PredicateDefinitionVo notEqual = new PredicateDefinitionVo();
        notEqual.setArgumentNumber("2");
        notEqual.setName("notEqual");
        notEqual.setLatexPattern("#1 \\ \\neq  \\ #2");
        definitions.put("notEqual_2", notEqual);
    }

    /**
     * Prints a LaTeX file into a given output stream.
     *
     * @param   language        Filter text to get and produce text in this language only.
     * @param   level           Filter for this detail level. TODO mime 20050205: not supported yet.
     * @param   outputStream    Write output herein.
     * @throws  IOException
     */
    public final synchronized void printLatex(final String language, final String level,
            final OutputStream outputStream) throws IOException {
        if (language == null) {
            this.language = "en";
        } else {
            this.language = language;
        }
        if (level == null) {
            this.level = "1";
        } else {
            this.level = level;
        }
        this.printer = new PrintStream(outputStream);
        printLatexHeader();
        printQedeqHeader();
        printQedeqChapters();
        printQedeqBibliography();
        printLatexTrailer();
        if (printer.checkError()) {
            throw new IOException("TODO mime: better use another OutputStream");
        }
    }

    /**
     * Prints the header.
     */
    private void printQedeqHeader() {
        final LatexList title = qedeq.getHeader().getTitle();
        printer.print("\\title{");
        printer.print(getLatexListEntry(title));
        printer.println("}");
        printer.println("\\author{");
        final AuthorList authors = qedeq.getHeader().getAuthorList();
        for (int i = 0; i < authors.size(); i++) {
            final Author author = authors.get(i);
            printer.println(author.getName().getLatex());
        }
        printer.println("}");
        printer.println();
        printer.println("\\begin{document}");
        printer.println();
        printer.println("\\maketitle");
        printer.println();
        printer.println("\\setlength{\\parskip}{0pt}");
        printer.println("\\tableofcontents");
        printer.println("\\setlength{\\parskip}{5pt plus 2pt minus 1pt}");
        printer.println();
    }

    /**
     * Print all chapters.
     */
    private void printQedeqChapters() {
        final ChapterList chapters = qedeq.getChapterList();
        for (int i = 0; i < chapters.size(); i++) {
            final Chapter chapter = chapters.get(i);
            printer.print("\\chapter");
            if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) {
                printer.print("*");
            }
            printer.print("{");
            printer.print(getLatexListEntry(chapter.getTitle()));
            final String label = "chapter" + i;
            printer.println("} \\label{" + label + "} \\hypertarget{" + label + "}{}");
            if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) {
                printer.println("\\addcontentsline{toc}{chapter}{"
                    + getLatexListEntry(chapter.getTitle()) + "}");
            }
            printer.println();
            if (chapter.getIntroduction() != null) {
                printer.println(getLatexListEntry(chapter.getIntroduction()));
                printer.println();
            }
            final SectionList sections = chapter.getSectionList();
            if (sections != null) {
                printSections(i, sections);
                printer.println();
            }
            printer.println("%% end of chapter " + getLatexListEntry(chapter.getTitle()));
            printer.println();
        }
    }

    /**
     * Print bibliography (if any).
     */
    private void printQedeqBibliography() {
        final LiteratureItemList items = qedeq.getLiteratureItemList();
        if (items == null) {
            return;
        }
        printer.println("\\begin{thebibliography}{99}");
        for (int i = 0; i < items.size(); i++) {
            final LiteratureItem item = items.get(i);
            printer.print("\\bibitem{" + item.getLabel() + "} ");
            printer.println(getLatexListEntry(item.getItem()));
            printer.println();
        }
        printer.println("\\end{thebibliography}");
        // TODO mime 20060926: remove language dependency
        if ("de".equals(language)) {
            printer.println("\\addcontentsline{toc}{chapter}{Literaturverzeichnis}");
        } else {
            printer.println("\\addcontentsline{toc}{chapter}{Bibliography}");
        }

    }

    /**
     * Print all given sections.
     *
     * @param   chapter     Chapter number.
     * @param   sections    List of sections.
     */
    private void printSections(final int chapter, final SectionList sections) {
        if (sections == null) {
            return;
        }
        for (int i = 0; i < sections.size(); i++) {
            final Section section = sections.get(i);
            printer.print("\\section{");
            printer.print(getLatexListEntry(section.getTitle()));
            final String label = "chapter" + chapter + "_section" + i;
            printer.println("} \\label{" + label + "} \\hypertarget{" + label + "}{}");
            printer.println(getLatexListEntry(section.getIntroduction()));
            printer.println();
            printSubsections(section.getSubsectionList());
        }
    }

    /**
     * Print all given subsections.
     *
     * @param   nodes   List of subsections.
     */
    private void printSubsections(final SubsectionList nodes) {
        if (nodes == null) {
            return;
        }
        for (int i = 0; i < nodes.size(); i++) {
            final SubsectionType subsectionType = nodes.get(i);
            if (subsectionType instanceof Node) {
                final Node node = (Node) subsectionType;
                printer.println("\\par");
                printer.println(getLatexListEntry(node.getPrecedingText()));
                printer.println();
                final String id = node.getId();
                final NodeType type = node.getNodeType();
                String title = null;
                if (node.getTitle() != null) {
                    title = getLatexListEntry(node.getTitle());
                }
                if (type instanceof Axiom) {
                    printAxiom((Axiom) type, title, id);
                } else if (type instanceof PredicateDefinition) {
                    printPredicateDefinition((PredicateDefinition) type, title, id);
                } else if (type instanceof FunctionDefinition) {
                    printFunctionDefinition((FunctionDefinition) type, title, id);
                } else if (type instanceof Proposition) {
                    printProposition((Proposition) type, title, id);
                } else if (type instanceof Rule) {
                    printRule((Rule) type, title, id);
                } else {
                    throw new RuntimeException((type != null ? "unknown type: "
                        + type.getClass().getName() : "node type empty"));
                }
                printer.println();
                printer.println(getLatexListEntry(node.getSucceedingText()));
            } else {
                final Subsection subsection = (Subsection) subsectionType;
                if (subsection.getTitle() != null) {
                    printer.print("\\subsection{");
                    printer.println(getLatexListEntry(subsection.getTitle()));
                    printer.println("}");
                }
                printer.println(getLatexListEntry(subsection.getLatex()));
            }
            printer.println();
            printer.println();
        }
    }

    /**
     * Print axiom.
     *
     * @param   axiom   Print this.
     * @param   title   Extra name.
     * @param   id      Label for marking this axiom.
     */
    private void printAxiom(final Axiom axiom, final String title, final String id) {
        printer.println("\\begin{ax}" + (title != null ? "[" + title + "]" : ""));
        printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
        printFormula(axiom.getFormula().getElement());
        printer.println(getLatexListEntry(axiom.getDescription()));
        printer.println("\\end{ax}");
    }

    /**
     * Print top level formula. If the formula has the form <code>AND(.., .., ..)</code> the
     * formula is broken down in several labeled lines.
     *
     * @param   element     Formula to print.
     * @param   mainLabel   Main formula label.
     */
    private void printTopFormula(final Element element, final String mainLabel) {
        if (!element.isList() || !element.getList().getOperator().equals("AND")) {
            printFormula(element);
            return;
        }
        final ElementList list = element.getList();
        printer.println("\\mbox{}");
        printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{0.9\\linewidth}l}}");
        for (int i = 0; i < list.size(); i++)  {
            final String label = (i < ALPHABET.length() ? "" + ALPHABET .charAt(i) : "" + i);
            printer.println("\\centering $" + getLatex(list.getElement(i)) + "$"
                + " & \\label{" + mainLabel + ":" + label + "} \\hypertarget{" + mainLabel + ":"
                + label + "}{} \\mbox{\\emph{(" + label + ")}} "
                + (i + 1 < list.size() ? "\\\\" : ""));
        }
        printer.println("\\end{longtable}");
    }

    /**
     * Print formula.
     *
     * @param   element Formula to print.
     */
    private void printFormula(final Element element) {
        printer.println("\\mbox{}");
        printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{\\linewidth}}}");
        printer.println("\\centering $" + getLatex(element) + "$");
        printer.println("\\end{longtable}");
    }

    /**
     * Print predicate definition.
     *
     * @param   definition  Print this.
     * @param   title       Extra name.
     * @param   id          Label for marking this definition.
     */
    private void printPredicateDefinition(final PredicateDefinition definition, final String title,
            final String id) {
        final StringBuffer define = new StringBuffer("$$" + definition.getLatexPattern());
        final VariableList list = definition.getVariableList();
        if (list != null) {
            for (int i = list.size() - 1; i >= 0; i--) {
                Trace.trace(this, "printPredicateDefinition", "replacing!");
                ReplaceUtility.replace(define, "#" + (i + 1), getLatex(list.get(i)));
            }
        }
        if (definition.getFormula() != null) {
            printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : ""));
            printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
            define.append("\\ :\\leftrightarrow \\ ");
            define.append(getLatex(definition.getFormula().getElement()));
        } else {
            printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : ""));
            printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
        }
        define.append("$$");
        definitions.put(definition.getName() + "_" + definition.getArgumentNumber(), definition);
        Trace.param(this, "printPredicateDefinition", "define", define);
        printer.println(define);
        printer.println(getLatexListEntry(definition.getDescription()));
        if (definition.getFormula() != null) {
            printer.println("\\end{defn}");
        } else {
            printer.println("\\end{idefn}");
        }
    }

    /**
     * Print function definition.
     *
     * @param   definition  Print this.
     * @param   title       Extra name.
     * @param   id          Label for marking this definition.
     */
    private void printFunctionDefinition(final FunctionDefinition definition, final String title,
            final String id) {
        final StringBuffer define = new StringBuffer("$$" + definition.getLatexPattern());
        final VariableList list = definition.getVariableList();
        if (list != null) {
            for (int i = list.size() - 1; i >= 0; i--) {
                Trace.trace(this, "printFunctionDefinition", "replacing!");
                ReplaceUtility.replace(define, "#" + (i + 1), getLatex(list.get(i)));
            }
        }
        if (definition.getTerm() != null) {
            printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : ""));
            printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
            define.append("\\ := \\ ");
            define.append(getLatex(definition.getTerm().getElement()));
        } else {
            printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : ""));
            printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
        }
        define.append("$$");
        definitions.put(definition.getName() + "_" + definition.getArgumentNumber(), definition);
        Trace.param(this, "printFunctionDefinition", "define", define);
        printer.println(define);
        printer.println(getLatexListEntry(definition.getDescription()));
        if (definition.getTerm() != null) {
            printer.println("\\end{defn}");
        } else {
            printer.println("\\end{idefn}");
        }
    }

    /**
     * Print proposition.
     *
     * @param   proposition Print this.
     * @param   title       Extra name.
     * @param   id          Label for marking this proposition.
     */
    private void printProposition(final Proposition proposition, final String title,
            final String id) {
        printer.println("\\begin{prop}" + (title != null ? "[" + title + "]" : ""));
        printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
        printTopFormula(proposition.getFormula().getElement(), id);
        printer.println(getLatexListEntry(proposition.getDescription()));
        printer.println("\\end{prop}");
        if (proposition.getProofList() != null) {
            for (int i = 0; i < proposition.getProofList().size(); i++) {
                printer.println("\\begin{proof}");
                printer.println(getLatexListEntry(proposition.getProofList().get(i)
                    .getNonFormalProof()));
                printer.println("\\end{proof}");
            }
        }
    }

    /**
     * Print rule declaration.
     *
     * @param   rule        Print this.
     * @param   title       Extra name.
     * @param   id          Label for marking this proposition.
     */
    private void printRule(final Rule rule, final String title,
            final String id) {
        printer.println("\\begin{rul}" + (title != null ? "[" + title + "]" : ""));
        printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
        printer.println(getLatexListEntry(rule.getDescription()));
        printer.println("\\end{rul}");

// TODO mime 20051210: are these informations equivalent to a formal proof?
/*
        if (null != rule.getLinkList()) {
            printer.println("\\begin{proof}");
            printer.println("Rule name: " + rule.getName());
            printer.println();
            printer.println();
            for (int i = 0; i < rule.getLinkList().size(); i++) {
                printer.println(rule.getLinkList().get(i));
            }
            printer.println("\\end{proof}");
        }
*/
        if (rule.getProofList() != null) {
            for (int i = 0; i < rule.getProofList().size(); i++) {
                printer.println("\\begin{proof}");
                printer.println(getLatexListEntry(rule.getProofList().get(i)
                    .getNonFormalProof()));
                printer.println("\\end{proof}");
            }
        }
    }

    /**
     * Get LaTeX element presentation.
     *
     * @param   element    Print this element.
     * @return  LaTeX form of element.
     */
    private String getLatex(final Element element) {
        return getLatex(element, true);
    }

    /**
     * Get LaTeX element presentation.
     *
     * @param   element Print this element.
     * @param   first   First level?
     * @return  LaTeX form of element.
     */
    private String getLatex(final Element element, final boolean first) {
        final StringBuffer buffer = new StringBuffer();
        if (element.isAtom()) {
            return element.getAtom().getString();
        }
        final ElementList list = element.getList();
        if (list.getOperator().equals("PREDCON")) {
            final String identifier = list.getElement(0).getAtom().getString() + "_"
                + (list.size() - 1);
            // TODO mime 20060922: is only working for definition name + argument number
            //  if argument length is dynamic this dosen't work
            if (definitions.containsKey(identifier)) {
                final PredicateDefinition definition = (PredicateDefinition)
                definitions.get(identifier);
                final StringBuffer define = new StringBuffer(definition.getLatexPattern());
                for (int i = list.size() - 1; i >= 1; i--) {
                    ReplaceUtility.replace(define, "#" + i, getLatex(list.getElement(i), false));
                }
                buffer.append(define);
            } else {
                buffer.append(identifier);
                buffer.append("(");
                for (int i = 1; i < list.size(); i++) {
                    buffer.append(getLatex(list.getElement(i), false));
                    if (i + 1 < list.size()) {
                        buffer.append(", ");
                    }
                }
                buffer.append(")");
            }
        } else if (list.getOperator().equals("PREDVAR")) {
            final String identifier = list.getElement(0).getAtom().getString();
            buffer.append(identifier);
            if (list.size() > 1) {
                buffer.append("(");
                for (int i = 1; i < list.size(); i++) {
                    buffer.append(getLatex(list.getElement(i), false));
                    if (i + 1 < list.size()) {
                        buffer.append(", ");
                    }
                }
                buffer.append(")");
            }
        } else if (list.getOperator().equals("FUNCON")) {
            final String identifier = list.getElement(0).getAtom().getString() + "_"
                + (list.size() - 1);
            // TODO mime 20060922: is only working for definition name + argument number
            //  if argument length is dynamic this dosen't work
            if (definitions.containsKey(identifier)) {
                final FunctionDefinition definition = (FunctionDefinition)
                    definitions.get(identifier);
                final StringBuffer define = new StringBuffer(definition.getLatexPattern());
                for (int i = list.size() - 1; i >= 1; i--) {
                    ReplaceUtility.replace(define, "#" + i, getLatex(list.getElement(i), false));
                }
                buffer.append(define);
            } else {
                buffer.append(identifier);
                buffer.append("(");
                for (int i = 1; i < list.size(); i++) {
                    buffer.append(getLatex(list.getElement(i), false));
                    if (i + 1 < list.size()) {
                        buffer.append(", ");
                    }
                }
                buffer.append(")");
            }
        } else if (list.getOperator().equals("FUNVAR")) {
            final String identifier = list.getElement(0).getAtom().getString();
            buffer.append(identifier);
            if (list.size() > 1) {
                buffer.append("(");
                for (int i = 1; i < list.size(); i++) {
                    buffer.append(getLatex(list.getElement(i), false));
                    if (i + 1 < list.size()) {
                        buffer.append(", ");
                    }
                }
                buffer.append(")");
            }
        } else if (list.getOperator().equals("VAR")) {
            final String text = list.getElement(0).getAtom().getString();
            // interpret variable identifier as number
            try {
                final int index = Integer.parseInt(text);
                final String newText = "" + index;
                if (!text.equals(newText) || newText.startsWith("-")) {
                    throw new NumberFormatException("This is no allowed number: " + text);
                }
                switch (index) {
                case 1:
                    return "x";
                case 2:
                    return "y";
                case 3:
                    return "z";
                case 4:
                    return "u";
                case 5:
                    return "v";
                case 6:
                    return "w";
                default:
                    return "x_" + (index - 6);
                }
            } catch (NumberFormatException e) {
                // variable identifier is no number, just take it as it is
                return text;
            }
        } else if (list.getOperator().equals("AND") || list.getOperator().equals("OR")
                || list.getOperator().equals("EQUI") || list.getOperator().equals("IMPL")) {
            final String infix;
            if (list.getOperator().equals("AND")) {
                infix = "\\ \\land \\ ";
            } else if (list.getOperator().equals("OR")) {
                infix = "\\ \\lor \\ ";
            } else if (list.getOperator().equals("EQUI")) {
                infix = "\\ \\leftrightarrow \\ ";
            } else {
                infix = "\\ \\rightarrow \\ ";
            }
            if (!first) {
                buffer.append("(");
            }
            for (int i = 0; i < list.size(); i++) {
                buffer.append(getLatex(list.getElement(i), false));
                if (i + 1 < list.size()) {
                    buffer.append(infix);
                }
            }
            if (!first) {
                buffer.append(")");
            }
        } else if (list.getOperator().equals("FORALL") || list.getOperator().equals("EXISTS")
                || list.getOperator().equals("EXISTSU")) {
            final String prefix;
            if (list.getOperator().equals("FORALL")) {
                prefix = "\\forall ";
            } else if (list.getOperator().equals("EXISTS")) {
                prefix = "\\exists ";
            } else {
                prefix = "\\exists! ";
            }
            buffer.append(prefix);
            for (int i = 0; i < list.size(); i++) {
                if (i != 0 || (i == 0 && list.size() <= 2)) {
                    buffer.append(getLatex(list.getElement(i), false));
                }
                if (i + 1 < list.size()) {
                    buffer.append("\\ ");
                }
                if (list.size() > 2 && i == 1) {
                    buffer.append("\\ ");
                }
            }
        } else if (list.getOperator().equals("NOT")) {
            final String prefix = "\\neg ";
            buffer.append(prefix);
            for (int i = 0; i < list.size(); i++) {
                buffer.append(getLatex(list.getElement(i), false));
            }
        } else if (list.getOperator().equals("CLASS")) {
            final String prefix = "\\{ ";
            buffer.append(prefix);
            for (int i = 0; i < list.size(); i++) {
                buffer.append(getLatex(list.getElement(i), false));
                if (i + 1 < list.size()) {
                    buffer.append(" \\ | \\ ");
                }
            }
            buffer.append(" \\} ");
        } else if (list.getOperator().equals("CLASSLIST")) {
            final String prefix = "\\{ ";
            buffer.append(prefix);
            for (int i = 0; i < list.size(); i++) {
                buffer.append(getLatex(list.getElement(i), false));
                if (i + 1 < list.size()) {
                    buffer.append(", \\ ");
                }
            }
            buffer.append(" \\} ");
        } else if (list.getOperator().equals("QUANTOR_INTERSECTION")) {
            final String prefix = "\\bigcap";
            buffer.append(prefix);
            if (0 < list.size()) {
                buffer.append("{").append(getLatex(list.getElement(0), false)).append("}");
            }
            for (int i = 1; i < list.size(); i++) {
                buffer.append(getLatex(list.getElement(i), false));
                if (i + 1 < list.size()) {
                    buffer.append(" \\ \\ ");
                }
            }
            buffer.append(" \\} ");
        } else if (list.getOperator().equals("QUANTOR_UNION")) {
            final String prefix = "\\bigcup";
            buffer.append(prefix);
            if (0 < list.size()) {
                buffer.append("{").append(getLatex(list.getElement(0), false)).append("}");
            }
            for (int i = 1; i < list.size(); i++) {
                buffer.append(getLatex(list.getElement(i), false));
                if (i + 1 < list.size()) {
                    buffer.append(" \\ \\ ");
                }
            }
            buffer.append(" \\} ");
        } else {
            buffer.append(list.getOperator());
            buffer.append("(");
            for (int i = 0; i < list.size(); i++) {
                buffer.append(getLatex(list.getElement(i), false));
                if (i + 1 < list.size()) {
                    buffer.append(", ");
                }
            }
            buffer.append(")");
        }
        return buffer.toString();
    }

    /**
     * Print LaTeX lines for the file head.
     */
    private void printLatexHeader() {
        printer.println("% -*- TeX:" + language.toUpperCase() + " -*-");
        printer.println("%%% ====================================================================");
        printer.println("%%% @LaTeX-file " + getFileName());
        printer.println("%%% Generated at " + getTimestamp());
        printer.println("%%% ====================================================================");
        printer.println();
        printer.println(
            "%%% Permission is granted to copy, distribute and/or modify this document");
        printer.println("%%% under the terms of the GNU Free Documentation License, Version 1.2");
        printer.println("%%% or any later version published by the Free Software Foundation;");
        printer.println(
            "%%% with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts.");
        printer.println();
        printer.println("\\documentclass[a4paper,german,10pt,twoside]{book}");
        if ("de".equals(language)) {
            printer.println("\\usepackage[german]{babel}");
        } else if ("en".equals(language)) {
            printer.println("\\usepackage[english]{babel}");
        } else {
            printer.println("%%% TODO unknown language: " + language);
            printer.println("%%% TODO using default language");
            printer.println("\\usepackage[english]{babel}");
        }
        printer.println("\\usepackage{makeidx}");
        printer.println("\\usepackage{amsmath,amsthm,amssymb}");
        printer.println("\\usepackage{color}");
        printer.println("\\usepackage[bookmarks,bookmarksnumbered,bookmarksopen,");
        printer.println("   colorlinks,linkcolor=webgreen,pagebackref]{hyperref}");
        printer.println("\\definecolor{webgreen}{rgb}{0,.5,0}");
        printer.println("\\usepackage{graphicx}");
        printer.println("\\usepackage{xr}");
        printer.println("\\usepackage{epsfig,longtable}");
        printer.println("\\usepackage{tabularx}");
        printer.println();
        if ("de".equals(language)) {
            printer.println("\\newtheorem{thm}{Theorem}[chapter]");
            printer.println("\\newtheorem{cor}[thm]{Korollar}");
            printer.println("\\newtheorem{lem}[thm]{Lemma}");
            printer.println("\\newtheorem{prop}[thm]{Proposition}");
            printer.println("\\newtheorem{ax}{Axiom}");
            printer.println("\\newtheorem{rul}{Regel}");
            printer.println();
            printer.println("\\theoremstyle{definition}");
            printer.println("\\newtheorem{defn}[thm]{Definition}");
            printer.println("\\newtheorem{idefn}[thm]{Initiale Definition}");
            printer.println();
            printer.println("\\theoremstyle{remark}");
            printer.println("\\newtheorem{rem}[thm]{Bemerkung}");
            printer.println("\\newtheorem*{notation}{Notation}");
        } else if ("en".equals(language)) {
            printer.println("\\newtheorem{thm}{Theorem}[chapter]");
            printer.println("\\newtheorem{cor}[thm]{Corollary}");
            printer.println("\\newtheorem{lem}[thm]{Lemma}");
            printer.println("\\newtheorem{prop}[thm]{Proposition}");
            printer.println("\\newtheorem{ax}{Axiom}");
            printer.println("\\newtheorem{rul}{Rule}");
            printer.println();
            printer.println("\\theoremstyle{definition}");
            printer.println("\\newtheorem{defn}[thm]{Definition}");
            printer.println("\\newtheorem{idefn}[thm]{Initial Definition}");
            printer.println();
            printer.println("\\theoremstyle{remark}");
            printer.println("\\newtheorem{rem}[thm]{Remark}");
            printer.println("\\newtheorem*{notation}{Notation}");
        } else {
            printer.println("%%% TODO unknown language: " + language);
            printer.println("%%% TODO using default language");
            printer.println("\\newtheorem{thm}{Theorem}[chapter]");
            printer.println("\\newtheorem{cor}[thm]{Corollary}");
            printer.println("\\newtheorem{lem}[thm]{Lemma}");
            printer.println("\\newtheorem{prop}[thm]{Proposition}");
            printer.println("\\newtheorem{ax}{Axiom}");
            printer.println();
            printer.println("\\theoremstyle{definition}");
            printer.println("\\newtheorem{defn}[thm]{Definition}");
            printer.println("\\newtheorem{idefn}[thm]{Initial Definition}");
            printer.println();
            printer.println("\\theoremstyle{remark}");
            printer.println("\\newtheorem{rem}[thm]{Remark}");
            printer.println("\\newtheorem*{notation}{Notation}");
        }
        printer.println();
        printer.println("\\addtolength{\\textheight}{7\\baselineskip}");
        printer.println("\\addtolength{\\topmargin}{-5\\baselineskip}");
        printer.println();
        printer.println("\\setlength{\\parindent}{0pt}");
        printer.println();
        printer.println("\\frenchspacing \\sloppy");
        printer.println();
        printer.println("\\makeindex");
        printer.println();
        printer.println();
    }

    /**
     * Print LaTeX trailer.
     */
    private void printLatexTrailer() {
        printer.println("\\backmatter");
        printer.println();
        printer.println("\\addcontentsline{toc}{chapter}{\\indexname} \\printindex");
        printer.println();
        printer.println("\\end{document}");
        printer.println();
    }

    /**
     * Get regular name for the LaTeX file.
     *
     * @return  File name.
     */
    private String getFileName() {
        // FIXME mime 20050805: add language, validate with currently used file name e.g.
        // qedeq_basic_concept_en.tex
        return qedeq.getHeader().getSpecification().getName() + "_"
            + qedeq.getHeader().getSpecification().getRuleVersion() + ".tex";
    }

    /**
     * Get timestamp.
     *
     * @return  Current timestamp.
     */
    private String getTimestamp() {
        final SimpleDateFormat formatter = new SimpleDateFormat("yyyy-MM-dd' 'HH:mm:ss,SSS");
        return formatter.format(new Date());
    }

    /**
     * Filters correct entry out of LaTeX list. Filter criterion is for example the correct
     * language.
     * TODO mime 20050205: filter level too?
     *
     * @param   list    List of LaTeX texts.
     * @return  Filtered text.
     */
    private String getLatexListEntry(final LatexList list) {
        if (list == null) {
            return "";
        }
        for (int i = 0; i < list.size(); i++) {
            if (language.equals(list.get(i).getLanguage())) {
                return getLatex(list.get(i));
            }
        }
        // assume entry with missing language as default
        for (int i = 0; i < list.size(); i++) {
            if (list.get(i).getLanguage() == null) {
                return getLatex(list.get(i));
            }
        }
        for (int i = 0; i < list.size(); i++) { // TODO mime 20050222: evaluate default?
            return "MISSING! OTHER: " + getLatex(list.get(i));
        }
        return "MISSING!";
    }

    /**
     * Get really LaTeX. Does some simple character replacements for umlauts.
     * TODO mime 20050205: filter more than German umlauts
     *
     * @param   latex   Unescaped text.
     * @return  Really LaTeX.
     */
    private String getLatex(final Latex latex) {
        if (latex.getLatex() == null) {
            return "";
        }
        final StringBuffer buffer = new StringBuffer(latex.getLatex());
        IoUtility.deleteLineLeadingWhitespace(buffer);
        ReplaceUtility.replace(buffer, "\u00fc", "{\\\"u}");
        ReplaceUtility.replace(buffer, "\u00f6", "{\\\"o}");
        ReplaceUtility.replace(buffer, "\u00e4", "{\\\"a}");
        ReplaceUtility.replace(buffer, "\u00dc", "{\\\"U}");
        ReplaceUtility.replace(buffer, "\u00d6", "{\\\"O}");
        ReplaceUtility.replace(buffer, "\u00c4", "{\\\"A}");
        ReplaceUtility.replace(buffer, "\u00df", "{\\ss}");
        return buffer.toString();
    }

}