0001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
0002 *
0003 * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
0004 *
0005 * "Hilbert II" is free software; you can redistribute
0006 * it and/or modify it under the terms of the GNU General Public
0007 * License as published by the Free Software Foundation; either
0008 * version 2 of the License, or (at your option) any later version.
0009 *
0010 * This program is distributed in the hope that it will be useful,
0011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
0012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
0013 * GNU General Public License for more details.
0014 */
0015
0016 package org.qedeq.kernel.bo.service.latex;
0017
0018 import java.io.File;
0019 import java.io.FileInputStream;
0020 import java.io.FileOutputStream;
0021 import java.io.IOException;
0022 import java.io.InputStream;
0023 import java.util.Locale;
0024
0025 import org.qedeq.base.io.IoUtility;
0026 import org.qedeq.base.io.Parameters;
0027 import org.qedeq.base.io.SourcePosition;
0028 import org.qedeq.base.io.TextInput;
0029 import org.qedeq.base.io.TextOutput;
0030 import org.qedeq.base.trace.Trace;
0031 import org.qedeq.base.utility.DateUtility;
0032 import org.qedeq.base.utility.EqualsUtility;
0033 import org.qedeq.base.utility.StringUtility;
0034 import org.qedeq.kernel.bo.log.QedeqLog;
0035 import org.qedeq.kernel.bo.module.ControlVisitor;
0036 import org.qedeq.kernel.bo.module.InternalServiceProcess;
0037 import org.qedeq.kernel.bo.module.KernelNodeBo;
0038 import org.qedeq.kernel.bo.module.KernelQedeqBo;
0039 import org.qedeq.kernel.bo.module.PluginExecutor;
0040 import org.qedeq.kernel.bo.module.Reference;
0041 import org.qedeq.kernel.se.base.list.Element;
0042 import org.qedeq.kernel.se.base.list.ElementList;
0043 import org.qedeq.kernel.se.base.module.Add;
0044 import org.qedeq.kernel.se.base.module.Author;
0045 import org.qedeq.kernel.se.base.module.AuthorList;
0046 import org.qedeq.kernel.se.base.module.Axiom;
0047 import org.qedeq.kernel.se.base.module.ChangedRule;
0048 import org.qedeq.kernel.se.base.module.ChangedRuleList;
0049 import org.qedeq.kernel.se.base.module.Chapter;
0050 import org.qedeq.kernel.se.base.module.Conclusion;
0051 import org.qedeq.kernel.se.base.module.ConditionalProof;
0052 import org.qedeq.kernel.se.base.module.Existential;
0053 import org.qedeq.kernel.se.base.module.FormalProof;
0054 import org.qedeq.kernel.se.base.module.FormalProofLine;
0055 import org.qedeq.kernel.se.base.module.FormalProofLineList;
0056 import org.qedeq.kernel.se.base.module.FunctionDefinition;
0057 import org.qedeq.kernel.se.base.module.Header;
0058 import org.qedeq.kernel.se.base.module.Hypothesis;
0059 import org.qedeq.kernel.se.base.module.Import;
0060 import org.qedeq.kernel.se.base.module.ImportList;
0061 import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
0062 import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
0063 import org.qedeq.kernel.se.base.module.Latex;
0064 import org.qedeq.kernel.se.base.module.LatexList;
0065 import org.qedeq.kernel.se.base.module.LinkList;
0066 import org.qedeq.kernel.se.base.module.LiteratureItem;
0067 import org.qedeq.kernel.se.base.module.LiteratureItemList;
0068 import org.qedeq.kernel.se.base.module.LocationList;
0069 import org.qedeq.kernel.se.base.module.ModusPonens;
0070 import org.qedeq.kernel.se.base.module.Node;
0071 import org.qedeq.kernel.se.base.module.PredicateDefinition;
0072 import org.qedeq.kernel.se.base.module.Proof;
0073 import org.qedeq.kernel.se.base.module.Proposition;
0074 import org.qedeq.kernel.se.base.module.Qedeq;
0075 import org.qedeq.kernel.se.base.module.Rename;
0076 import org.qedeq.kernel.se.base.module.Rule;
0077 import org.qedeq.kernel.se.base.module.Section;
0078 import org.qedeq.kernel.se.base.module.SectionList;
0079 import org.qedeq.kernel.se.base.module.Specification;
0080 import org.qedeq.kernel.se.base.module.Subsection;
0081 import org.qedeq.kernel.se.base.module.SubsectionList;
0082 import org.qedeq.kernel.se.base.module.SubsectionType;
0083 import org.qedeq.kernel.se.base.module.SubstFree;
0084 import org.qedeq.kernel.se.base.module.SubstFunc;
0085 import org.qedeq.kernel.se.base.module.SubstPred;
0086 import org.qedeq.kernel.se.base.module.Universal;
0087 import org.qedeq.kernel.se.base.module.UsedByList;
0088 import org.qedeq.kernel.se.common.ModuleAddress;
0089 import org.qedeq.kernel.se.common.ModuleContext;
0090 import org.qedeq.kernel.se.common.ModuleDataException;
0091 import org.qedeq.kernel.se.common.Plugin;
0092 import org.qedeq.kernel.se.common.RuleKey;
0093 import org.qedeq.kernel.se.common.SourceFileExceptionList;
0094
0095
0096 /**
0097 * Transfer a QEDEQ module into a LaTeX file.
0098 * <p>
0099 * <b>This is just a quick written generator. No parsing or validation
0100 * of inline LaTeX text is done. This class just generates some LaTeX output to be able to
0101 * get a visual impression of a QEDEQ module.</b>
0102 *
0103 * @author Michael Meyling
0104 */
0105 public final class Qedeq2LatexExecutor extends ControlVisitor implements PluginExecutor {
0106
0107 /** This class. */
0108 private static final Class CLASS = Qedeq2LatexExecutor.class;
0109
0110 // TODO m31 20100316: check number area for error codes
0111 // TODO m31 20100803: add JUnit tests for all error codes
0112
0113 /** Output goes here. */
0114 private TextOutput printer;
0115
0116 /** Filter text to get and produce text in this language. */
0117 private String language;
0118
0119 /** Filter for this detail level. */
0120 // private String level;
0121
0122 /** Should additional information be put into LaTeX output? E.g. QEDEQ reference names. */
0123 private final boolean info;
0124
0125 /** Should only names and formulas be be printed? */
0126 private final boolean brief;
0127
0128 /** Current node id. */
0129 private String id;
0130
0131 /** Current node title. */
0132 private String title;
0133
0134 /** Sub context like "getIntroduction()". */
0135 private String subContext = "";
0136
0137 /** Remembered proof line label. */
0138 private String label = "";
0139
0140 /** Remembered proof line formula. */
0141 private String formula = "";
0142
0143 /** Remembered proof line reason. */
0144 private String reason = "";
0145
0146 /** Remembered proof line tabulator level. */
0147 private int tabLevel = 0;
0148
0149 /** Alphabet for tagging. */
0150 private static final String ALPHABET = "abcdefghijklmnopqrstuvwxyz";
0151
0152 /**
0153 * Constructor.
0154 *
0155 * @param plugin This plugin we work for.
0156 * @param prop QEDEQ BO object.
0157 * @param parameters Parameters.
0158 */
0159 public Qedeq2LatexExecutor(final Plugin plugin, final KernelQedeqBo prop, final Parameters parameters) {
0160 super(plugin, prop);
0161 info = parameters.getBoolean("info");
0162 brief = parameters.getBoolean("brief");
0163 }
0164
0165 public Object executePlugin(final InternalServiceProcess process, final Object data) {
0166 final String method = "executePlugin(QedeqBo, Map)";
0167 try {
0168 QedeqLog.getInstance().logRequest("Generate LaTeX", getQedeqBo().getUrl());
0169 final String[] languages = getQedeqBo().getSupportedLanguages();
0170 for (int j = 0; j < languages.length; j++) {
0171 language = languages[j];
0172 // level = "1";
0173 final String result = generateLatex(process, languages[j], "1").toString();
0174 if (languages[j] != null) {
0175 QedeqLog.getInstance().logSuccessfulReply(
0176 "LaTeX for language \"" + languages[j]
0177 + "\" was generated from into \"" + result + "\"", getQedeqBo().getUrl());
0178 } else {
0179 QedeqLog.getInstance().logSuccessfulReply(
0180 "LaTeX for default language "
0181 + "was generated into \"" + result + "\"", getQedeqBo().getUrl());
0182 }
0183 }
0184 if (languages.length == 0) {
0185 QedeqLog.getInstance().logMessage("no supported language found, assuming 'en'");
0186 final String result = generateLatex(process, "en", "1").toString();
0187 QedeqLog.getInstance().logSuccessfulReply(
0188 "LaTeX for language \"en"
0189 + "\" was generated into \"" + result + "\"", getQedeqBo().getUrl());
0190 }
0191 } catch (final SourceFileExceptionList e) {
0192 final String msg = "Generation failed";
0193 Trace.fatal(CLASS, this, method, msg, e);
0194 QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(), e.getMessage());
0195 } catch (IOException e) {
0196 final String msg = "Generation failed";
0197 Trace.fatal(CLASS, this, method, msg, e);
0198 QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(), e.getMessage());
0199 } catch (final RuntimeException e) {
0200 Trace.fatal(CLASS, this, method, "unexpected problem", e);
0201 QedeqLog.getInstance().logFailureReply(
0202 "Generation failed", getQedeqBo().getUrl(), "unexpected problem: "
0203 + (e.getMessage() != null ? e.getMessage() : e.toString()));
0204 }
0205 return null;
0206 }
0207
0208 /**
0209 * Get an input stream for the LaTeX creation.
0210 *
0211 * @param process This process executes us.
0212 * @param language Filter text to get and produce text in this language only.
0213 * @param level Filter for this detail level. LATER mime 20050205: not supported
0214 * yet.
0215 * @return Resulting LaTeX.
0216 * @throws SourceFileExceptionList Major problem occurred.
0217 * @throws IOException File IO failed.
0218 */
0219 public InputStream createLatex(final InternalServiceProcess process, final String language, final String level)
0220 throws SourceFileExceptionList, IOException {
0221 return new FileInputStream(generateLatex(process, language, level));
0222 }
0223
0224 /**
0225 * Gives a LaTeX representation of given QEDEQ module as InputStream.
0226 *
0227 * @param process This process executes us.
0228 * @param language Filter text to get and produce text in this language only.
0229 * <code>null</code> is ok.
0230 * @param level Filter for this detail level. LATER mime 20050205: not supported
0231 * yet.
0232 * @return Resulting LaTeX.
0233 * @throws SourceFileExceptionList Major problem occurred.
0234 * @throws IOException File IO failed.
0235 */
0236 public File generateLatex(final InternalServiceProcess process, final String language, final String level)
0237 throws SourceFileExceptionList, IOException {
0238 final String method = "generateLatex(String, String)";
0239 this.language = language;
0240 // this.level = level;
0241 // first we try to get more information about required modules and their predicates..
0242 try {
0243 getServices().loadRequiredModules(getQedeqBo(), process);
0244 getServices().checkWellFormedness(getQedeqBo(), process);
0245 } catch (Exception e) {
0246 // we continue and ignore external predicates
0247 Trace.trace(CLASS, method, e);
0248 }
0249 String tex = getQedeqBo().getModuleAddress().getFileName();
0250 if (tex.toLowerCase(Locale.US).endsWith(".xml")) {
0251 tex = tex.substring(0, tex.length() - 4);
0252 }
0253 if (language != null && language.length() > 0) {
0254 tex = tex + "_" + language;
0255 }
0256 // the destination is the configured destination directory plus the (relative)
0257 // localized file (or path) name
0258 File destination = new File(getServices().getConfig()
0259 .getGenerationDirectory(), tex + ".tex").getCanonicalFile();
0260
0261 init();
0262
0263 try {
0264 // TODO 20110204 m31: here we should choose the correct encoding; perhaps GUI configurable?
0265 if ("de".equals(language)) {
0266 printer = new TextOutput(getQedeqBo().getName(), new FileOutputStream(destination),
0267 "ISO-8859-1") {
0268 public void append(final String txt) {
0269 super.append(escapeUmlauts(txt));
0270 }
0271 };
0272 } else {
0273 printer = new TextOutput(getQedeqBo().getName(), new FileOutputStream(destination),
0274 "UTF-8") {
0275 public void append(final String txt) {
0276 super.append(escapeUmlauts(txt));
0277 }
0278 };
0279 }
0280 traverse(process);
0281 } finally {
0282 getQedeqBo().addPluginErrorsAndWarnings(getPlugin(), getErrorList(), getWarningList());
0283 if (printer != null) {
0284 printer.flush();
0285 printer.close();
0286 }
0287 }
0288 if (printer != null && printer.checkError()) {
0289 throw printer.getError();
0290 }
0291 try {
0292 QedeqBoDuplicateLanguageChecker.check(process, getPlugin(), getQedeqBo());
0293 } catch (SourceFileExceptionList warnings) {
0294 getQedeqBo().addPluginErrorsAndWarnings(getPlugin(), null, warnings);
0295 }
0296 return destination.getCanonicalFile();
0297 }
0298
0299 /**
0300 * Reset counters and other variables. Should be executed before {@link #traverse()}.
0301 */
0302 protected void init() {
0303 id = null;
0304 title = null;
0305 subContext = "";
0306 }
0307
0308 public final void visitEnter(final Qedeq qedeq) {
0309 printer.println("% -*- TeX"
0310 + (language != null ? ":" + language.toUpperCase(Locale.US) : "") + " -*-");
0311 printer.println("%%% ====================================================================");
0312 printer.println("%%% @LaTeX-file " + printer.getName());
0313 printer.println("%%% Generated from " + getQedeqBo().getModuleAddress());
0314 printer.println("%%% Generated at " + DateUtility.getTimestamp());
0315 printer.println("%%% ====================================================================");
0316 printer.println();
0317 printer.println(
0318 "%%% Permission is granted to copy, distribute and/or modify this document");
0319 printer.println("%%% under the terms of the GNU Free Documentation License, Version 1.2");
0320 printer.println("%%% or any later version published by the Free Software Foundation;");
0321 printer.println(
0322 "%%% with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts.");
0323 printer.println();
0324 printer.println("\\documentclass[a4paper,german,10pt,twoside]{book}");
0325 if ("de".equals(language)) {
0326 printer.println("\\usepackage[german]{babel}");
0327 } else {
0328 if (!"en".equals(language)) {
0329 printer.println("%%% TODO unknown language: " + language);
0330 }
0331 printer.println("\\usepackage[english]{babel}");
0332 }
0333 printer.println("\\usepackage{makeidx}");
0334 printer.println("\\usepackage{amsmath,amsthm,amssymb}");
0335 printer.println("\\usepackage{color}");
0336 printer.println("\\usepackage{xr}");
0337 printer.println("\\usepackage{tabularx}");
0338 // printer.println("\\usepackage{epsfig,longtable}");
0339 // printer.println("\\usepackage{ltabptch}"); // not installed on our server
0340 printer.println("\\usepackage[bookmarks=true,bookmarksnumbered,bookmarksopen,");
0341 printer.println(" unicode=true,colorlinks=true,linkcolor=webgreen,");
0342 printer.println(" pagebackref=true,pdfnewwindow=true,pdfstartview=FitH]{hyperref}");
0343 printer.println("\\definecolor{webgreen}{rgb}{0,.5,0}");
0344 printer.println("\\usepackage{epsfig,longtable}");
0345 printer.println("\\usepackage{graphicx}");
0346 printer.println("\\usepackage[all]{hypcap}");
0347 printer.println();
0348 if ("de".equals(language)) {
0349 // TODO m31 20100313: validate different counter types
0350 // printer.println("\\newtheorem{thm}{Theorem}[chapter]");
0351 printer.println("\\newtheorem{thm}{Theorem}");
0352 printer.println("\\newtheorem{cor}[thm]{Korollar}");
0353 printer.println("\\newtheorem{lem}[thm]{Lemma}");
0354 printer.println("\\newtheorem{prop}[thm]{Proposition}");
0355 printer.println("\\newtheorem{ax}{Axiom}");
0356 printer.println("\\newtheorem{rul}{Regel}");
0357 printer.println();
0358 printer.println("\\theoremstyle{definition}");
0359 printer.println("\\newtheorem{defn}{Definition}");
0360 printer.println("\\newtheorem{idefn}[defn]{Initiale Definition}");
0361 printer.println();
0362 printer.println("\\theoremstyle{remark}");
0363 printer.println("\\newtheorem{rem}[thm]{Bemerkung}");
0364 printer.println("\\newtheorem*{notation}{Notation}");
0365 } else {
0366 if (!"en".equals(language)) {
0367 printer.println("%%% TODO unknown language: " + language);
0368 }
0369 // TODO m31 20100313: validate different counter types
0370 // printer.println("\\newtheorem{thm}{Theorem}[chapter]");
0371 printer.println("\\newtheorem{thm}{Theorem}");
0372 printer.println("\\newtheorem{cor}[thm]{Corollary}");
0373 printer.println("\\newtheorem{lem}[thm]{Lemma}");
0374 printer.println("\\newtheorem{prop}[thm]{Proposition}");
0375 printer.println("\\newtheorem{ax}{Axiom}");
0376 printer.println("\\newtheorem{rul}{Rule}");
0377 printer.println();
0378 printer.println("\\theoremstyle{definition}");
0379 printer.println("\\newtheorem{defn}{Definition}");
0380 printer.println("\\newtheorem{idefn}[defn]{Initial Definition}");
0381 printer.println();
0382 printer.println("\\theoremstyle{remark}");
0383 printer.println("\\newtheorem{rem}[thm]{Remark}");
0384 printer.println("\\newtheorem*{notation}{Notation}");
0385 }
0386 printer.println();
0387 printer.println();
0388 printer.println("\\addtolength{\\textheight}{7\\baselineskip}");
0389 printer.println("\\addtolength{\\topmargin}{-5\\baselineskip}");
0390 printer.println();
0391 printer.println("\\setlength{\\parindent}{0pt}");
0392 printer.println();
0393 printer.println("\\frenchspacing \\sloppy");
0394 printer.println();
0395 printer.println("\\makeindex");
0396 printer.println();
0397 printer.println();
0398 }
0399
0400 public final void visitLeave(final Qedeq qedeq) {
0401 printer.println("\\addcontentsline{toc}{chapter}{\\indexname} \\printindex");
0402 printer.println();
0403 printer.println("\\end{document}");
0404 printer.println();
0405 }
0406
0407 public void visitEnter(final Header header) {
0408 final LatexList tit = header.getTitle();
0409 printer.print("\\title{");
0410 printer.print(getLatexListEntry("getTitle()", tit));
0411 printer.println("}");
0412 printer.println("\\author{");
0413 final AuthorList authors = getQedeqBo().getQedeq().getHeader().getAuthorList();
0414 final StringBuffer authorList = new StringBuffer();
0415 for (int i = 0; i < authors.size(); i++) {
0416 if (i > 0) {
0417 authorList.append(", ");
0418 printer.println(", ");
0419 }
0420 final Author author = authors.get(i);
0421 final String name = author.getName().getLatex().trim();
0422 printer.print(name);
0423 authorList.append(name);
0424 String email = author.getEmail();
0425 if (email != null && email.trim().length() > 0) {
0426 authorList.append(" \\href{mailto:" + email + "}{" + email + "}");
0427 }
0428 }
0429 printer.println();
0430 printer.println("}");
0431 printer.println();
0432 printer.println("\\begin{document}");
0433 printer.println();
0434 printer.println("\\maketitle");
0435 printer.println();
0436 printer.println("\\setlength{\\parskip}{5pt plus 2pt minus 1pt}");
0437 printer.println("\\mbox{}");
0438 printer.println("\\vfill");
0439 printer.println();
0440 final String url = getQedeqBo().getUrl();
0441 if (url != null && url.length() > 0) {
0442 printer.println("\\par");
0443 if ("de".equals(language)) {
0444 printer.println("Die Quelle f{\"ur} dieses Dokument ist hier zu finden:");
0445 } else {
0446 if (!"en".equals(language)) {
0447 printer.println("%%% TODO unknown language: " + language);
0448 }
0449 printer.println("The source for this document can be found here:");
0450 }
0451 printer.println("\\par");
0452 printer.println("\\url{" + url + "}");
0453 printer.println();
0454 }
0455 {
0456 printer.println("\\par");
0457 if ("de".equals(language)) {
0458 printer.println("Die vorliegende Publikation ist urheberrechtlich gesch{\"u}tzt.");
0459 } else {
0460 if (!"en".equals(language)) {
0461 printer.println("%%% TODO unknown language: " + language);
0462 }
0463 printer.println("Copyright by the authors. All rights reserved.");
0464 }
0465 }
0466 final String email = header.getEmail();
0467 if (email != null && email.length() > 0) {
0468 final String emailUrl = "\\href{mailto:" + email + "}{" + email + "}";
0469 printer.println("\\par");
0470 if ("de".equals(language)) {
0471 printer.println("Bei Fragen, Anregungen oder Bitte um Aufnahme in die Liste der"
0472 + " abh\u00e4ngigen Module schicken Sie bitte eine EMail an die Adresse "
0473 + emailUrl);
0474 printer.println();
0475 printer.println("\\par");
0476 printer.println("Die Autoren dieses Dokuments sind:");
0477 printer.println(authorList);
0478 } else {
0479 if (!"en".equals(language)) {
0480 printer.println("%%% TODO unknown language: " + language);
0481 }
0482 printer.println("If you have any questions, suggestions or want to add something"
0483 + " to the list of modules that use this one, please send an email to the"
0484 + " address " + emailUrl);
0485 printer.println();
0486 printer.println("\\par");
0487 printer.println("The authors of this document are:");
0488 printer.println(authorList);
0489 }
0490 printer.println();
0491 }
0492 }
0493
0494 public void visitLeave(final Header header) {
0495 printer.println();
0496 printer.println();
0497 printer.println("\\setlength{\\parskip}{0pt}");
0498 printer.println("\\tableofcontents");
0499 printer.println();
0500 printer.println("\\setlength{\\parskip}{5pt plus 2pt minus 1pt}");
0501 printer.println();
0502 }
0503
0504 public void visitEnter(final ImportList imports) throws ModuleDataException {
0505 printer.println();
0506 printer.println();
0507 printer.println("\\par");
0508 if ("de".equals(language)) {
0509 printer.println("Benutzte QEDEQ module:");
0510 } else {
0511 if (!"en".equals(language)) {
0512 printer.println("%%% TODO unknown language: " + language);
0513 }
0514 printer.println("Used other QEDEQ modules:");
0515 }
0516 printer.println();
0517 printer.println("\\par");
0518 printer.println();
0519 }
0520
0521 public void visitEnter(final Import imp) throws ModuleDataException {
0522 printer.println();
0523 printer.println("\\par");
0524 printer.print("\\textbf{" + imp.getLabel() + "} ");
0525 final Specification spec = imp.getSpecification();
0526 printer.print(getLatex(spec.getName()));
0527 if (spec.getLocationList() != null && spec.getLocationList().size() > 0
0528 && spec.getLocationList().get(0).getLocation().length() > 0) {
0529 printer.print(" ");
0530 printer.print("\\url{" + getPdfLink((KernelQedeqBo) getQedeqBo()
0531 .getLabels().getReferences().getQedeqBo(imp.getLabel())) + "}");
0532 }
0533 printer.println();
0534 }
0535
0536 /**
0537 * Get URL for QEDEQ XML module.
0538 *
0539 * @param address Current module address.
0540 * @param specification Find URL for this location list.
0541 * @return URL or <code>""</code> if none (valid?) was found.
0542 */
0543 private String getUrl(final ModuleAddress address, final Specification specification) {
0544 final LocationList list = specification.getLocationList();
0545 if (list == null || list.size() <= 0) {
0546 return "";
0547 }
0548 try {
0549 return address.getModulePaths(specification)[0].getUrl();
0550 } catch (IOException e) {
0551 return "";
0552 }
0553 }
0554
0555 public void visitEnter(final Chapter chapter) {
0556 // check if we print only brief and test for non text subnodes
0557 if (brief) {
0558 boolean hasFormalContent = false;
0559 do {
0560 final SectionList sections = chapter.getSectionList();
0561 if (sections == null) {
0562 break;
0563 }
0564 for (int i = 0; i < sections.size() && !hasFormalContent; i++) {
0565 final Section section = sections.get(i);
0566 if (section == null) {
0567 continue;
0568 }
0569 final SubsectionList subSections = section.getSubsectionList();
0570 if (subSections == null) {
0571 continue;
0572 }
0573 for (int j = 0; j < subSections.size(); j++) {
0574 final SubsectionType subSection = subSections.get(j);
0575 if (!(subSection instanceof Subsection)) {
0576 hasFormalContent = true;
0577 break;
0578 }
0579 }
0580 }
0581 } while (false);
0582 if (!hasFormalContent) {
0583 setBlocked(true);
0584 return;
0585 }
0586 }
0587 printer.print("\\chapter");
0588 if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) {
0589 printer.print("*");
0590 }
0591 printer.print("{");
0592 printer.print(getLatexListEntry("getTitle()", chapter.getTitle()));
0593 final String chapterLabel = "chapter" + getCurrentNumbers().getAbsoluteChapterNumber();
0594 printer.println("} \\label{" + chapterLabel + "} \\hypertarget{" + chapterLabel + "}{}");
0595 if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) {
0596 printer.println("\\addcontentsline{toc}{chapter}{"
0597 + getLatexListEntry("getTitle()", chapter.getTitle()) + "}");
0598 }
0599 printer.println();
0600 if (chapter.getIntroduction() != null && !brief) {
0601 printer.println(getLatexListEntry("getIntroduction()", chapter.getIntroduction()));
0602 printer.println();
0603 }
0604 }
0605
0606 public void visitLeave(final Chapter chapter) {
0607 printer.println("%% end of chapter " + getLatexListEntry("getTitle()", chapter.getTitle()));
0608 printer.println();
0609 setBlocked(false);
0610 }
0611
0612 public void visitLeave(final SectionList list) {
0613 printer.println();
0614 }
0615
0616 public void visitEnter(final Section section) {
0617 // check if we print only brief and test for non text subnodes
0618 if (brief) {
0619 boolean hasFormalContent = false;
0620 do {
0621 final SubsectionList subSections = section.getSubsectionList();
0622 if (subSections == null) {
0623 break;
0624 }
0625 for (int j = 0; j < subSections.size(); j++) {
0626 final SubsectionType subSection = subSections.get(j);
0627 if (!(subSection instanceof Subsection)) {
0628 hasFormalContent = true;
0629 break;
0630 }
0631 }
0632 } while (false);
0633 if (!hasFormalContent) {
0634 setBlocked(true);
0635 return;
0636 }
0637 }
0638 printer.print("\\section");
0639 if (section.getNoNumber() != null && section.getNoNumber().booleanValue()) {
0640 printer.print("*");
0641 }
0642 printer.print("{");
0643 printer.print(getLatexListEntry("getTitle()", section.getTitle()));
0644 final String chapterLabel = "chapter" + getCurrentNumbers().getAbsoluteChapterNumber()
0645 + "_section" + getCurrentNumbers().getAbsoluteSectionNumber();
0646 printer.println("} \\label{" + chapterLabel + "} \\hypertarget{" + chapterLabel + "}{}");
0647 if (section.getIntroduction() != null && !brief) {
0648 printer.println(getLatexListEntry("getIntroduction()", section.getIntroduction()));
0649 printer.println();
0650 }
0651 }
0652
0653 public void visitLeave(final Section section) {
0654 setBlocked(false);
0655 }
0656
0657 public void visitEnter(final Subsection subsection) {
0658 /* LATER mime 20070131: use this information?
0659 if (subsection.getId() != null) {
0660 printer.print(" id=\"" + subsection.getId() + "\"");
0661 }
0662 if (subsection.getLevel() != null) {
0663 printer.print(" level=\"" + subsection.getLevel() + "\"");
0664 }
0665 */
0666 if (brief) {
0667 return;
0668 }
0669 if (subsection.getTitle() != null) {
0670 printer.print("\\subsection{");
0671 printer.println(getLatexListEntry("getTitle()", subsection.getTitle()));
0672 printer.println("}");
0673 }
0674 if (subsection.getId() != null) {
0675 printer.println("\\label{" + subsection.getId() + "} \\hypertarget{"
0676 + subsection.getId() + "}{}");
0677 }
0678 printer.println(getLatexListEntry("getLatex()", subsection.getLatex()));
0679 }
0680
0681 public void visitLeave(final Subsection subsection) {
0682 if (brief) {
0683 return;
0684 }
0685 printer.println();
0686 printer.println();
0687 }
0688
0689 public void visitEnter(final Node node) {
0690 /** TODO mime 20070131: level filter
0691 if (node.getLevel() != null) {
0692 printer.print(" level=\"" + node.getLevel() + "\"");
0693 }
0694 */
0695 if (node.getPrecedingText() != null && !brief) {
0696 printer.println("\\par");
0697 printer.println(getLatexListEntry("getPrecedingText()", node.getPrecedingText()));
0698 printer.println();
0699 }
0700 id = node.getId();
0701 title = null;
0702 if (node.getTitle() != null) {
0703 title = getLatexListEntry("getTitle()", node.getTitle());
0704 }
0705 }
0706
0707 public void visitLeave(final Node node) {
0708 printer.println();
0709 if (node.getSucceedingText() != null && !brief) {
0710 printer.println(getLatexListEntry("getSucceedingText()", node.getSucceedingText()));
0711 printer.println();
0712 }
0713 printer.println();
0714 }
0715
0716 public void visitEnter(final Axiom axiom) {
0717 printer.println("\\begin{ax}" + (title != null ? "[" + title + "]" : ""));
0718 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
0719 if (info) {
0720 printer.println("{\\tt \\tiny [\\verb]" + id + "]]}");
0721 }
0722 printFormula(axiom.getFormula().getElement());
0723 printer.println(getLatexListEntry("getDescription()", axiom.getDescription()));
0724 printer.println("\\end{ax}");
0725 }
0726
0727 public void visitEnter(final Proposition proposition) {
0728 printer.println("\\begin{prop}" + (title != null ? "[" + title + "]" : ""));
0729 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
0730 if (info) {
0731 printer.println("{\\tt \\tiny [\\verb]" + id + "]]}");
0732 }
0733 printTopFormula(proposition.getFormula().getElement(), id);
0734 printer.println(getLatexListEntry("getDescription()", proposition.getDescription()));
0735 printer.println("\\end{prop}");
0736 }
0737
0738 public void visitEnter(final Proof proof) {
0739 /* LATER mime 20070131: filter level and kind
0740 if (proof.getKind() != null) {
0741 printer.print(" kind=\"" + proof.getKind() + "\"");
0742 }
0743 if (proof.getLevel() != null) {
0744 printer.print(" level=\"" + proof.getLevel() + "\"");
0745 }
0746 */
0747 if (brief) {
0748 setBlocked(true);
0749 return;
0750 }
0751 printer.println("\\begin{proof}");
0752 printer.println(getLatexListEntry("getNonFormalProof()", proof.getNonFormalProof()));
0753 printer.println("\\end{proof}");
0754 }
0755
0756 public void visitLeave(final Proof proof) {
0757 setBlocked(false);
0758 }
0759
0760 public void visitEnter(final FormalProof proof) {
0761 if (brief) {
0762 setBlocked(true);
0763 return;
0764 }
0765 tabLevel = 0;
0766 printer.println("\\begin{proof}");
0767 // if ("de".equals(language)) {
0768 // printer.println("Beweis (formal):");
0769 // } else {
0770 // printer.println("Proof (formal):");
0771 // }
0772 }
0773
0774 public void visitEnter(final FormalProofLineList lines) {
0775 if (tabLevel == 0) {
0776 printer.println("\\mbox{}\\\\");
0777 printer.println("\\begin{longtable}[h!]{r@{\\extracolsep{\\fill}}p{9cm}@{\\extracolsep{\\fill}}p{4cm}}");
0778 }
0779 }
0780
0781 public void visitLeave(final FormalProofLineList lines) {
0782 if (tabLevel == 0) {
0783 printer.println(" & & \\qedhere");
0784 printer.println("\\end{longtable}");
0785 }
0786 }
0787
0788 public void visitEnter(final FormalProofLine line) {
0789 if (line.getLabel() != null) {
0790 label = line.getLabel();
0791 } else {
0792 label = "";
0793 }
0794 if (line.getFormula() != null) {
0795 formula = "$" + getQedeqBo().getElement2Latex().getLatex(line.getFormula().getElement()) + "$";
0796 } else {
0797 formula = "";
0798 }
0799 if (line.getReason() != null) {
0800 reason = line.getReason().toString();
0801 } else {
0802 reason = "";
0803 }
0804 }
0805
0806 public void visitLeave(final FormalProofLine line) {
0807 if (brief) {
0808 return;
0809 }
0810 linePrintln();
0811 }
0812
0813 /**
0814 * Print proof line made out of label, formula and reason.
0815 */
0816 private void linePrintln() {
0817 if (formula.length() == 0 && reason.length() == 0) {
0818 return;
0819 }
0820 if (label.length() > 0) {
0821 String display = getNodeBo().getNodeVo().getId() + "!" + label;
0822 printer.print("\\label{" + display + "} \\hypertarget{" + display
0823 + "}{\\mbox{(" + label + ")}} ");
0824 }
0825 printer.print(" \\ & \\ ");
0826 for (int i = 0; i < tabLevel; i++) {
0827 printer.print("\\mbox{\\qquad}");
0828 }
0829 if (formula.length() > 0) {
0830 printer.print(formula);
0831 }
0832 printer.print(" \\ & \\ ");
0833 if (reason.length() > 0) {
0834 printer.print("{\\tiny ");
0835 printer.print(reason);
0836 printer.print("}");
0837 }
0838 printer.println(" \\\\ ");
0839 reason = "";
0840 formula = "";
0841 label = "";
0842 }
0843
0844 private String getReference(final String reference) {
0845 return getReference(reference, "getReference()");
0846 }
0847
0848 private String getReference(final String reference, final String subContext) {
0849 final String context = getCurrentContext().getLocationWithinModule();
0850 try {
0851 getCurrentContext().setLocationWithinModule(context + "." + subContext);
0852 return (getReference(reference, null, null));
0853 } finally {
0854 getCurrentContext().setLocationWithinModule(context);
0855 }
0856 }
0857
0858 public void visitEnter(final ModusPonens r) throws ModuleDataException {
0859 if (brief) {
0860 return;
0861 }
0862 reason = getRuleReference(r.getName());
0863 boolean one = false;
0864 if (r.getReference1() != null) {
0865 reason += " " + getReference(r.getReference1(), "getReference1()");
0866 one = true;
0867 }
0868 if (r.getReference1() != null) {
0869 if (one) {
0870 reason += ",";
0871 }
0872 reason += " " + getReference(r.getReference2(), "getReference2()");
0873 }
0874 }
0875
0876 public void visitEnter(final Add r) throws ModuleDataException {
0877 if (brief) {
0878 return;
0879 }
0880 reason = getRuleReference(r.getName());
0881 if (r.getReference() != null) {
0882 reason += " " + getReference(r.getReference());
0883 }
0884 }
0885
0886 public void visitEnter(final Rename r) throws ModuleDataException {
0887 if (brief) {
0888 return;
0889 }
0890 reason = getRuleReference(r.getName());
0891 if (r.getOriginalSubjectVariable() != null) {
0892 reason += " $" + getQedeqBo().getElement2Latex().getLatex(
0893 r.getOriginalSubjectVariable()) + "$";
0894 }
0895 if (r.getReplacementSubjectVariable() != null) {
0896 reason += " by $" + getQedeqBo().getElement2Latex().getLatex(
0897 r.getReplacementSubjectVariable()) + "$";
0898 }
0899 if (r.getReference() != null) {
0900 reason += " in " + getReference(r.getReference());
0901 }
0902 }
0903
0904 public void visitEnter(final SubstFree r) throws ModuleDataException {
0905 if (brief) {
0906 return;
0907 }
0908 reason = getRuleReference(r.getName());
0909 if (r.getSubjectVariable() != null) {
0910 reason += " $" + getQedeqBo().getElement2Latex().getLatex(
0911 r.getSubjectVariable()) + "$";
0912 }
0913 if (r.getSubstituteTerm() != null) {
0914 reason += " by $" + getQedeqBo().getElement2Latex().getLatex(
0915 r.getSubstituteTerm()) + "$";
0916 }
0917 if (r.getReference() != null) {
0918 reason += " in " + getReference(r.getReference());
0919 }
0920 }
0921
0922 public void visitEnter(final SubstFunc r) throws ModuleDataException {
0923 if (brief) {
0924 return;
0925 }
0926 reason = getRuleReference(r.getName());
0927 if (r.getFunctionVariable() != null) {
0928 reason += " $" + getQedeqBo().getElement2Latex().getLatex(
0929 r.getFunctionVariable()) + "$";
0930 }
0931 if (r.getSubstituteTerm() != null) {
0932 reason += " by $" + getQedeqBo().getElement2Latex().getLatex(
0933 r.getSubstituteTerm()) + "$";
0934 }
0935 if (r.getReference() != null) {
0936 reason += " in " + getReference(r.getReference());
0937 }
0938 }
0939
0940 public void visitEnter(final SubstPred r) throws ModuleDataException {
0941 if (brief) {
0942 return;
0943 }
0944 reason = getRuleReference(r.getName());
0945 if (r.getPredicateVariable() != null) {
0946 reason += " $" + getQedeqBo().getElement2Latex().getLatex(
0947 r.getPredicateVariable()) + "$";
0948 }
0949 if (r.getSubstituteFormula() != null) {
0950 reason += " by $" + getQedeqBo().getElement2Latex().getLatex(
0951 r.getSubstituteFormula()) + "$";
0952 }
0953 if (r.getReference() != null) {
0954 reason += " in " + getReference(r.getReference());
0955 }
0956 }
0957
0958 public void visitEnter(final Existential r) throws ModuleDataException {
0959 if (brief) {
0960 return;
0961 }
0962 reason = getRuleReference(r.getName());
0963 if (r.getSubjectVariable() != null) {
0964 reason += " with $" + getQedeqBo().getElement2Latex().getLatex(
0965 r.getSubjectVariable()) + "$";
0966 }
0967 if (r.getReference() != null) {
0968 reason += " in " + getReference(r.getReference());
0969 }
0970 }
0971
0972 public void visitEnter(final Universal r) throws ModuleDataException {
0973 if (brief) {
0974 return;
0975 }
0976 reason = getRuleReference(r.getName());
0977 if (r.getSubjectVariable() != null) {
0978 reason += " with $" + getQedeqBo().getElement2Latex().getLatex(
0979 r.getSubjectVariable()) + "$";
0980 }
0981 if (r.getReference() != null) {
0982 reason += " in " + getReference(r.getReference());
0983 }
0984 }
0985
0986 public void visitEnter(final ConditionalProof r) throws ModuleDataException {
0987 if (brief) {
0988 return;
0989 }
0990 reason = getRuleReference(r.getName());
0991 printer.print(" \\ & \\ ");
0992 for (int i = 0; i < tabLevel; i++) {
0993 printer.print("\\mbox{\\qquad}");
0994 }
0995 printer.println("Conditional Proof");
0996 printer.print(" \\ & \\ ");
0997 printer.println(" \\\\ ");
0998 tabLevel++;
0999 }
1000
1001 public void visitLeave(final ConditionalProof proof) {
1002 if (brief) {
1003 return;
1004 }
1005 tabLevel--;
1006 }
1007
1008 public void visitEnter(final Hypothesis hypothesis) {
1009 if (brief) {
1010 return;
1011 }
1012 reason = "Hypothesis";
1013 if (hypothesis.getLabel() != null) {
1014 label = hypothesis.getLabel();
1015 }
1016 if (hypothesis.getFormula() != null) {
1017 formula = "$" + getQedeqBo().getElement2Latex().getLatex(
1018 hypothesis.getFormula().getElement()) + "$";
1019 }
1020 }
1021
1022 public void visitLeave(final Hypothesis hypothesis) {
1023 if (brief) {
1024 return;
1025 }
1026 linePrintln();
1027 }
1028
1029 public void visitEnter(final Conclusion conclusion) {
1030 if (brief) {
1031 return;
1032 }
1033 tabLevel--;
1034 reason = "Conclusion";
1035 if (conclusion.getLabel() != null) {
1036 label = conclusion.getLabel();
1037 }
1038 if (conclusion.getFormula() != null) {
1039 formula = "$" + getQedeqBo().getElement2Latex().getLatex(
1040 conclusion.getFormula().getElement()) + "$";
1041 }
1042 }
1043
1044 public void visitLeave(final Conclusion conclusion) {
1045 if (brief) {
1046 return;
1047 }
1048 linePrintln();
1049 tabLevel++;
1050 }
1051
1052 public void visitLeave(final FormalProof proof) {
1053 if (!getBlocked()) {
1054 printer.println("\\end{proof}");
1055 }
1056 setBlocked(false);
1057 }
1058
1059 public void visitEnter(final InitialPredicateDefinition definition) {
1060 printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : ""));
1061 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
1062 if (info) {
1063 printer.println("{\\tt \\tiny [\\verb]" + id + "]]}");
1064 }
1065 printer.print("$$");
1066 printer.println(getLatex(definition.getPredCon()));
1067 printer.println("$$");
1068 printer.println(getLatexListEntry("getDescription()", definition.getDescription()));
1069 printer.println("\\end{idefn}");
1070 }
1071
1072 public void visitEnter(final PredicateDefinition definition) {
1073 printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : ""));
1074 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
1075 if (info) {
1076 printer.println("{\\tt \\tiny [\\verb]" + id + "]]}");
1077 }
1078 printer.print("$$");
1079 printer.print(getLatex(definition.getFormula().getElement()));
1080 printer.println("$$");
1081 printer.println(getLatexListEntry("getDescription()", definition.getDescription()));
1082 printer.println("\\end{defn}");
1083 }
1084
1085 public void visitEnter(final InitialFunctionDefinition definition) {
1086 printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : ""));
1087 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
1088 if (info) {
1089 printer.println("{\\tt \\tiny [\\verb]" + id + "]]}");
1090 }
1091 printer.print("$$");
1092 printer.print(getLatex(definition.getFunCon()));
1093 printer.println("$$");
1094 printer.println(getLatexListEntry("getDescription()", definition.getDescription()));
1095 printer.println("\\end{defn}");
1096 }
1097
1098 public void visitEnter(final FunctionDefinition definition) {
1099 printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : ""));
1100 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
1101 if (info) {
1102 printer.println("{\\tt \\tiny [\\verb]" + id + "]]}");
1103 }
1104 printer.print("$$");
1105 printer.print(getLatex(definition.getFormula().getElement()));
1106 printer.println("$$");
1107 printer.println("\\end{defn}");
1108 }
1109
1110 public void visitLeave(final FunctionDefinition definition) {
1111 // nothing to do
1112 }
1113
1114 public void visitEnter(final Rule rule) {
1115 printer.println("\\begin{rul}" + (title != null ? "[" + title + "]" : ""));
1116 printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}");
1117 if (info) {
1118 printer.println("{\\tt \\tiny [\\verb]" + id + "]]}");
1119 }
1120 printer.println();
1121 printer.println("\\par");
1122 printer.println("{\\em "
1123 + (rule.getName() != null ? " Name: \\verb]" + rule.getName() + "]" : "")
1124 + (rule.getVersion() != null ? " - Version: \\verb]" + rule.getVersion() + "]" : "")
1125 + "}");
1126 printer.println();
1127 printer.println();
1128 printer.println(getLatexListEntry("getDescription()", rule.getDescription()));
1129 printer.println("\\end{rul}");
1130 }
1131
1132 public void visitLeave(final Rule rule) {
1133 // nothing to do
1134 }
1135
1136 public void visitEnter(final LinkList linkList) {
1137 if (linkList.size() <= 0) {
1138 return;
1139 }
1140 if ("de".equals(language)) {
1141 printer.println("Basierend auf: ");
1142 } else {
1143 if (!"en".equals(language)) {
1144 printer.println("%%% TODO unknown language: " + language);
1145 }
1146 printer.println("Based on: ");
1147 }
1148 for (int i = 0; i < linkList.size(); i++) {
1149 if (linkList.get(i) != null) {
1150 printer.print(" " + getReference(linkList.get(i), "get(" + i + ")"));
1151 }
1152 };
1153 printer.println();
1154 }
1155
1156 public void visitEnter(final ChangedRuleList list) {
1157 if (list.size() <= 0) {
1158 return;
1159 }
1160 if ("de".equals(language)) {
1161 printer.println("Die folgenden Regeln m\u00fcssen erweitert werden.");
1162 } else {
1163 if (!"en".equals(language)) {
1164 printer.println("%%% TODO unknown language: " + language);
1165 }
1166 printer.println("The following rules have to be extended.");
1167 }
1168 printer.println();
1169 }
1170
1171 public void visitEnter(final ChangedRule rule) {
1172 printer.println("\\par");
1173 printer.println("\\label{" + id + "!" + rule.getName() + "} \\hypertarget{" + id + "!"
1174 + rule.getName() + "}{}");
1175 printer.print("{\\em "
1176 + (rule.getName() != null ? " Name: \\verb]" + rule.getName() + "]" : "")
1177 + (rule.getVersion() != null ? " - Version: \\verb]" + rule.getVersion() + "]" : ""));
1178 RuleKey old = getLocalRuleKey(rule.getName());
1179 if (old == null && getQedeqBo().getExistenceChecker() != null) {
1180 old = getQedeqBo().getExistenceChecker().getParentRuleKey(rule.getName());
1181 }
1182 if (old != null) {
1183 printer.print(" - Old Version: "
1184 + getRuleReference(rule.getName(), old.getVersion()));
1185 }
1186 printer.println("}");
1187 rule.getName();
1188 printer.println();
1189 if (rule.getDescription() != null) {
1190 printer.println(getLatexListEntry("getDescription()", rule.getDescription()));
1191 printer.println();
1192 printer.println();
1193 }
1194 }
1195
1196
1197 public void visitEnter(final LiteratureItemList list) {
1198 printer.println("\\backmatter");
1199 printer.println();
1200 printer.println("\\begin{thebibliography}{99}");
1201 if ("de".equals(language)) {
1202 printer.println("\\addcontentsline{toc}{chapter}{Literaturverzeichnis}");
1203 } else {
1204 if (!"en".equals(language)) {
1205 printer.println("%%% TODO unknown language: " + language);
1206 }
1207 printer.println("\\addcontentsline{toc}{chapter}{Bibliography}");
1208 }
1209 final ImportList imports = getQedeqBo().getQedeq().getHeader().getImportList();
1210 if (imports != null && imports.size() > 0) {
1211 printer.println();
1212 printer.println();
1213 printer.println("%% Used other QEDEQ modules:");
1214 for (int i = 0; i < imports.size(); i++) {
1215 final Import imp = imports.get(i);
1216 printer.print("\\bibitem{" + imp.getLabel() + "} ");
1217 final Specification spec = imp.getSpecification();
1218 printer.print(getLatex(spec.getName()));
1219 if (spec.getLocationList() != null && spec.getLocationList().size() > 0
1220 && spec.getLocationList().get(0).getLocation().length() > 0) {
1221 printer.print(" ");
1222 // TODO m31 20070205, 2010727: later on here must stand the location that was used
1223 // to verify the document contents.
1224 // Also get other informations like authors, title, etc.
1225 // It might also be better to link to URL?
1226 // printer.print("\\url{" + getUrl(getQedeqBo().getModuleAddress(), spec) + "}");
1227 printer.print("\\url{" + getPdfLink((KernelQedeqBo) getQedeqBo()
1228 .getLabels().getReferences().getQedeqBo(imp.getLabel())) + "}");
1229 }
1230 printer.println();
1231 }
1232 printer.println();
1233 printer.println();
1234 printer.println("%% Other references:");
1235 printer.println();
1236 }
1237 }
1238
1239 public void visitLeave(final LiteratureItemList list) {
1240 final UsedByList usedby = getQedeqBo().getQedeq().getHeader().getUsedByList();
1241 if (usedby != null && usedby.size() > 0) {
1242 printer.println();
1243 printer.println();
1244 printer.println("%% QEDEQ modules that use this one:");
1245 for (int i = 0; i < usedby.size(); i++) {
1246 final Specification spec = usedby.get(i);
1247 printer.print("\\bibitem{" + spec.getName() + "} ");
1248 printer.print(getLatex(spec.getName()));
1249 final String url = getUrl(getQedeqBo().getModuleAddress(), spec);
1250 if (url != null && url.length() > 0) {
1251 printer.print(" ");
1252 printer.print("\\url{" + url + "}");
1253 }
1254 printer.println();
1255 }
1256 printer.println();
1257 printer.println();
1258 }
1259 printer.println("\\end{thebibliography}");
1260 }
1261
1262 public void visitEnter(final LiteratureItem item) {
1263 printer.print("\\bibitem{" + item.getLabel() + "} ");
1264 printer.println(getLatexListEntry("getItem()", item.getItem()));
1265 printer.println();
1266 }
1267
1268 /**
1269 * Print top level formula. If the formula has the form <code>AND(.., .., ..)</code> the
1270 * formula is broken down in several labeled lines.
1271 *
1272 * @param element Formula to print.
1273 * @param mainLabel Main formula label.
1274 */
1275 private void printTopFormula(final Element element, final String mainLabel) {
1276 if (!element.isList() || !element.getList().getOperator().equals("AND")) {
1277 printFormula(element);
1278 return;
1279 }
1280 final ElementList list = element.getList();
1281 printer.println("\\mbox{}");
1282 printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{0.9\\linewidth}l}}");
1283 for (int i = 0; i < list.size(); i++) {
1284 String newLabel = "";
1285 if (list.size() >= ALPHABET.length() * ALPHABET.length()) {
1286 newLabel = "" + (i + 1);
1287 } else {
1288 // TODO 20110303 m31: this dosn't work if we have more than 26 * 26 elements
1289 if (list.size() > ALPHABET.length()) {
1290 final int div = (i / ALPHABET.length());
1291 newLabel = "" + ALPHABET.charAt(div);
1292 }
1293 newLabel += ALPHABET.charAt(i % ALPHABET.length());
1294 }
1295 // final String label = (i < ALPHABET.length() ? "" + ALPHABET .charAt(i) : "" + i);
1296 printer.println("\\centering $" + getLatex(list.getElement(i)) + "$"
1297 + " & \\label{" + mainLabel + "/" + newLabel + "} \\hypertarget{" + mainLabel + "/"
1298 + newLabel + "}{} \\mbox{\\emph{(" + newLabel + ")}} "
1299 + (i + 1 < list.size() ? "\\\\" : ""));
1300 }
1301 printer.println("\\end{longtable}");
1302 }
1303
1304 /**
1305 * Print formula.
1306 *
1307 * @param element Formula to print.
1308 */
1309 private void printFormula(final Element element) {
1310 printer.println("\\mbox{}");
1311 printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{\\linewidth}}}");
1312 printer.println("\\centering $" + getLatex(element) + "$");
1313 printer.println("\\end{longtable}");
1314 }
1315
1316 /**
1317 * Get LaTeX element presentation.
1318 *
1319 * @param element Print this element.
1320 * @return LaTeX form of element.
1321 */
1322 private String getLatex(final Element element) {
1323 return getQedeqBo().getElement2Latex().getLatex(element);
1324 }
1325
1326 /**
1327 * Filters correct entry out of LaTeX list. Filter criterion is for example the correct
1328 * language.
1329 * TODO mime 20050205: filter level too?
1330 *
1331 * @param method This method was called. Used to get the correct sub context.
1332 * Should not be null. If it is empty the <code>subContext</code>
1333 * is not changed.
1334 * @param list List of LaTeX texts.
1335 * @return Filtered text.
1336 */
1337 private String getLatexListEntry(final String method, final LatexList list) {
1338 if (list == null) {
1339 return "";
1340 }
1341 if (method.length() > 0) {
1342 subContext = method;
1343 }
1344 try {
1345 for (int i = 0; language != null && i < list.size(); i++) {
1346 if (language.equals(list.get(i).getLanguage())) {
1347 if (method.length() > 0) {
1348 subContext = method + ".get(" + i + ")";
1349 }
1350 return getLatex(list.get(i));
1351 }
1352 }
1353 // OK, we didn't found the language, so we take the default language
1354 final String def = getQedeqBo().getOriginalLanguage();
1355 for (int i = 0; i < list.size(); i++) {
1356 if (EqualsUtility.equals(def, list.get(i).getLanguage())) {
1357 if (method.length() > 0) {
1358 subContext = method + ".get(" + i + ")";
1359 }
1360 return "MISSING! OTHER: " + getLatex(list.get(i));
1361 }
1362 }
1363 // OK, we didn't find wanted and default language, so we take the first non empty one
1364 for (int i = 0; i < list.size(); i++) {
1365 if (method.length() > 0) {
1366 subContext = method + ".get(" + i + ")";
1367 }
1368 if (null != list.get(i) && null != list.get(i).getLatex()
1369 && list.get(i).getLatex().trim().length() > 0) {
1370 return "MISSING! OTHER: " + getLatex(list.get(i));
1371 }
1372 }
1373 return "MISSING!";
1374 } finally {
1375 if (method.length() > 0) {
1376 subContext = "";
1377 }
1378 }
1379 }
1380
1381 /**
1382 * Get really LaTeX. Does some simple character replacements for umlauts. Also transforms
1383 * <code>\qref{key}</code> into LaTeX.
1384 *
1385 * @param latex Unescaped text.
1386 * @return Really LaTeX.
1387 */
1388 private String getLatex(final Latex latex) {
1389 if (latex == null || latex.getLatex() == null) {
1390 return "";
1391 }
1392 StringBuffer result = new StringBuffer(latex.getLatex());
1393
1394 // LATER mime 20080324: check if LaTeX is correct and no forbidden tags are used
1395
1396 transformQref(result);
1397
1398 return deleteLineLeadingWhitespace(result.toString());
1399 }
1400
1401 /**
1402 * Transform <code>\qref{key}</code> entries into common LaTeX code.
1403 *
1404 * LATER mime 20080324: write JUnitTests to be sure that no runtime exceptions are thrown if
1405 * reference is at end of latex etc.
1406 *
1407 * @param result Work on this buffer.
1408 */
1409 private void transformQref(final StringBuffer result) {
1410 final String method = "transformQref(StringBuffer)";
1411 final StringBuffer buffer = new StringBuffer(result.toString());
1412 final TextInput input = new TextInput(buffer);
1413 int last = 0;
1414 try {
1415 result.setLength(0);
1416 while (input.forward("\\qref{")) {
1417 final SourcePosition startPosition = input.getSourcePosition();
1418 final int start = input.getPosition();
1419 if (!input.forward("}")) {
1420 addWarning(LatexErrorCodes.QREF_END_NOT_FOUND_CODE,
1421 LatexErrorCodes.QREF_END_NOT_FOUND_TEXT, startPosition,
1422 input.getSourcePosition());
1423 continue;
1424 }
1425 String ref = input.getSubstring(start + "\\qref{".length(), input.getPosition()).trim();
1426 input.read(); // read }
1427 Trace.param(CLASS, this, method, "1 ref", ref);
1428 if (ref.length() == 0) {
1429 addWarning(LatexErrorCodes.QREF_EMPTY_CODE, LatexErrorCodes.QREF_EMPTY_TEXT,
1430 startPosition, input.getSourcePosition());
1431 continue;
1432 }
1433 if (ref.length() > 1024) {
1434 addWarning(LatexErrorCodes.QREF_END_NOT_FOUND_CODE,
1435 LatexErrorCodes.QREF_END_NOT_FOUND_TEXT, startPosition,
1436 input.getSourcePosition());
1437 continue;
1438 }
1439 if (ref.indexOf("{") >= 0) {
1440 addWarning(LatexErrorCodes.QREF_END_NOT_FOUND_CODE,
1441 LatexErrorCodes.QREF_END_NOT_FOUND_TEXT, startPosition,
1442 input.getSourcePosition());
1443 continue;
1444 }
1445 final int end = input.getPosition();
1446 final SourcePosition endPosition = input.getSourcePosition();
1447 result.append(buffer.substring(last, start));
1448 result.append(getReference(ref, startPosition, endPosition));
1449 last = end;
1450 }
1451 } finally { // thanks to findbugs
1452 IoUtility.close(input);
1453 if (last < buffer.length()) {
1454 result.append(buffer.substring(last));
1455 }
1456 }
1457 }
1458
1459 private String getReference(final String reference, final SourcePosition start, final SourcePosition end) {
1460 final String method = "getReference(String, String)";
1461 Trace.param(CLASS, this, method, "2 reference", reference); // qreference within module
1462
1463 final Reference ref = getReference(reference, getCurrentContext(start, end), true, false);
1464 if (ref.isNodeLocalReference() && ref.isSubReference()) {
1465 return "\\hyperlink{" + ref.getNodeLabel() + "/" + ref.getSubLabel() + "}{" + "("
1466 + ref.getSubLabel() + ")" + "}";
1467 }
1468
1469 if (ref.isNodeLocalReference() && ref.isProofLineReference()) {
1470 return "\\hyperlink{" + ref.getNodeLabel() + "!" + ref.getProofLineLabel() + "}{" + "("
1471 + ref.getProofLineLabel() + ")" + "}";
1472 }
1473
1474 if (!ref.isExternal()) {
1475 return "\\hyperlink{" + ref.getNodeLabel()
1476 + (ref.isSubReference() ? "/" + ref.getSubLabel() : "")
1477 + (ref.isProofLineReference() ? "!" + ref.getProofLineLabel() : "")
1478 + "}{"
1479 + getNodeDisplay(ref.getNodeLabel(), ref.getNode())
1480 + (ref.isSubReference() ? " (" + ref.getSubLabel() + ")" : "")
1481 + (ref.isProofLineReference() ? " (" + ref.getProofLineLabel() + ")" : "")
1482 + "}";
1483 }
1484
1485 // do we have an external module reference without node?
1486 if (ref.isExternalModuleReference()) {
1487 return "\\url{" + getPdfLink(ref.getExternalQedeq()) + "}~\\cite{"
1488 + ref.getExternalQedeqLabel() + "}";
1489 // if we want to show the text "description": \href{my_url}{description}
1490 }
1491
1492 String external = getPdfLink(ref.getExternalQedeq());
1493 if (external.startsWith("file://")) {
1494 external = "file:" + external.substring("file://".length());
1495 }
1496 return "\\hyperref{" + external + "}{}{"
1497 + ref.getNodeLabel()
1498 + (ref.isSubReference() ? "/" + ref.getSubLabel() : "")
1499 + (ref.isProofLineReference() ? "!" + ref.getProofLineLabel() : "")
1500 + "}{" + getNodeDisplay(ref.getNodeLabel(), ref.getNode())
1501 + (ref.isSubReference() ? " (" + ref.getSubLabel() + ")" : "")
1502 + (ref.isProofLineReference() ? " (" + ref.getProofLineLabel() + ")" : "")
1503 + "}~\\cite{" + ref.getExternalQedeqLabel() + "}";
1504 }
1505
1506 private String getNodeDisplay(final String label, final KernelNodeBo kNode) {
1507 return StringUtility.replace(getNodeDisplay(label, kNode, language), " ", "~");
1508 }
1509
1510 private String getRuleReference(final String ruleName) {
1511 return getRuleReference(ruleName, ruleName);
1512 }
1513
1514 private String getRuleReference(final String ruleName, final String caption) {
1515 final String method = "getRuleReference(String, String)";
1516 Trace.param(CLASS, this, method, "ruleName", ruleName);
1517 RuleKey key = getLocalRuleKey(ruleName);
1518 if (key == null && getQedeqBo().getExistenceChecker() != null) {
1519 key = getQedeqBo().getExistenceChecker().getParentRuleKey(ruleName);
1520 }
1521 if (key == null) {
1522 key = getQedeqBo().getLabels().getRuleKey(ruleName);
1523 }
1524 KernelQedeqBo qedeq = getQedeqBo();
1525 if (getQedeqBo().getExistenceChecker() != null) {
1526 qedeq = getQedeqBo().getExistenceChecker().getQedeq(key);
1527 }
1528 String localRef = getQedeqBo().getLabels().getRuleLabel(key);
1529 final String refRuleName = qedeq.getLabels().getRule(key).getName();
1530 if (!ruleName.equals(refRuleName)) {
1531 localRef += "!" + ruleName;
1532 }
1533 qedeq.getLabels().getRule(key).getName();
1534 boolean local = getQedeqBo().equals(qedeq);
1535 if (local) {
1536 return "\\hyperlink{" + localRef + "}{" + caption + "}";
1537 }
1538 String external = getPdfLink(qedeq);
1539 if (external.startsWith("file://")) {
1540 external = "file:" + external.substring("file://".length());
1541 }
1542 return "\\hyperref{" + external + "}{}{" + caption + "}{"
1543 + localRef + "}";
1544 }
1545
1546 /**
1547 * Get current module context. Uses sub context information.
1548 *
1549 * @param startDelta Skip position (relative to location start). Could be
1550 * <code>null</code>.
1551 * @param endDelta Mark until this column (relative to location start).
1552 * be <code>null</code>
1553 * @return Current module context.
1554 */
1555 public ModuleContext getCurrentContext(final SourcePosition startDelta,
1556 final SourcePosition endDelta) {
1557 if (subContext.length() == 0) {
1558 return super.getCurrentContext();
1559 }
1560 final ModuleContext c = new ModuleContext(super.getCurrentContext().getModuleLocation(),
1561 super.getCurrentContext().getLocationWithinModule() + "." + subContext,
1562 startDelta, endDelta);
1563 return c;
1564 }
1565
1566 // TODO 20110214 m31: decide about removal
1567 // public ModuleContext getCurrentContext() {
1568 // throw new IllegalStateException("programming error");
1569 // }
1570
1571
1572 /**
1573 * Add warning.
1574 *
1575 * @param code Warning code.
1576 * @param msg Warning message.
1577 * @param startDelta Skip position (relative to location start). Could be
1578 * <code>null</code>.
1579 * @param endDelta Mark until this column (relative to location start).
1580 * be <code>null</code>
1581 */
1582 private void addWarning(final int code, final String msg, final SourcePosition startDelta,
1583 final SourcePosition endDelta) {
1584 Trace.param(CLASS, this, "addWarning", "msg", msg);
1585 addWarning(new LatexContentException(code, msg, getCurrentContext(startDelta, endDelta)));
1586 }
1587
1588 /**
1589 * Get URL to for PDF version of module. If the referenced module doesn't
1590 * support the current language we switch to the original language.
1591 *
1592 * @param prop Get URL for this QEDEQ module.
1593 * @return URL to PDF.
1594 */
1595 private String getPdfLink(final KernelQedeqBo prop) {
1596 if (prop == null) {
1597 return "";
1598 }
1599 final String url = prop.getUrl();
1600 final int dot = url.lastIndexOf(".");
1601 if (prop.isSupportedLanguage(language)) {
1602 return url.substring(0, dot) + "_" + language + ".pdf";
1603 }
1604 final String a = prop.getOriginalLanguage();
1605 return url.substring(0, dot) + (a.length() > 0 ? "_" + a : "") + ".pdf";
1606 }
1607
1608 /**
1609 * Get LaTeX from string. Escapes common characters.
1610 * Also gets rid of leading spaces if they are equal among the lines.
1611 *
1612 * @param text Unescaped text.
1613 * @return LaTeX.
1614 */
1615 private String getLatex(final String text) {
1616 final StringBuffer buffer = new StringBuffer(text);
1617 StringUtility.replace(buffer, "\\", "\\textbackslash");
1618 StringUtility.replace(buffer, "$", "\\$");
1619 StringUtility.replace(buffer, "&", "\\&");
1620 StringUtility.replace(buffer, "%", "\\%");
1621 StringUtility.replace(buffer, "#", "\\#");
1622 StringUtility.replace(buffer, "_", "\\_");
1623 StringUtility.replace(buffer, "{", "\\{");
1624 StringUtility.replace(buffer, "}", "\\}");
1625 StringUtility.replace(buffer, "~", "\\textasciitilde");
1626 StringUtility.replace(buffer, "^", "\\textasciicircum");
1627 StringUtility.replace(buffer, "<", "\\textless");
1628 StringUtility.replace(buffer, ">", "\\textgreater");
1629 StringUtility.deleteLineLeadingWhitespace(buffer);
1630 return buffer.toString().trim();
1631 }
1632
1633 /**
1634 * Trims text. Also gets rid of leading spaces if they are equal among the lines.
1635 *
1636 * @param text Text.
1637 * @return Untrimed text.
1638 */
1639 private String deleteLineLeadingWhitespace(final String text) {
1640 final StringBuffer buffer = new StringBuffer(text);
1641 StringUtility.deleteLineLeadingWhitespace(buffer);
1642 return buffer.toString().trim();
1643 }
1644
1645 /**
1646 * Get really LaTeX. Does some simple character replacements for umlauts.
1647 * LATER mime 20050205: filter more than German umlauts
1648 *
1649 * @param nearlyLatex Unescaped text.
1650 * @return Really LaTeX.
1651 */
1652 private String escapeUmlauts(final String nearlyLatex) {
1653 if (nearlyLatex == null) {
1654 return "";
1655 }
1656 final StringBuffer buffer = new StringBuffer(nearlyLatex);
1657 // System.out.println("before");
1658 // System.out.println(buffer);
1659 // System.out.println();
1660 // System.out.println("after");
1661 // System.out.println(buffer);
1662 // System.out.println("*******************************************************************");
1663 StringUtility.replace(buffer, "\u00fc", "{\\\"u}");
1664 StringUtility.replace(buffer, "\u00f6", "{\\\"o}");
1665 StringUtility.replace(buffer, "\u00e4", "{\\\"a}");
1666 StringUtility.replace(buffer, "\u00dc", "{\\\"U}");
1667 StringUtility.replace(buffer, "\u00d6", "{\\\"O}");
1668 StringUtility.replace(buffer, "\u00c4", "{\\\"A}");
1669 StringUtility.replace(buffer, "\u00df", "{\\ss}");
1670 return buffer.toString();
1671 }
1672
1673 }
|