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