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