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