1 | /* This file is part of the project "Hilbert II" - http://www.qedeq.org |
2 | * |
3 | * Copyright 2000-2014, Michael Meyling <mime@qedeq.org>. |
4 | * |
5 | * "Hilbert II" is free software; you can redistribute |
6 | * it and/or modify it under the terms of the GNU General Public |
7 | * License as published by the Free Software Foundation; either |
8 | * version 2 of the License, or (at your option) any later version. |
9 | * |
10 | * This program is distributed in the hope that it will be useful, |
11 | * but WITHOUT ANY WARRANTY; without even the implied warranty of |
12 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
13 | * GNU General Public License for more details. |
14 | */ |
15 | |
16 | package org.qedeq.kernel.bo.service.latex; |
17 | |
18 | import java.io.File; |
19 | import java.io.FileInputStream; |
20 | import java.io.FileOutputStream; |
21 | import java.io.IOException; |
22 | import java.io.InputStream; |
23 | import java.util.Locale; |
24 | |
25 | import org.qedeq.base.io.IoUtility; |
26 | import org.qedeq.base.io.Parameters; |
27 | import org.qedeq.base.io.SourcePosition; |
28 | import org.qedeq.base.io.TextInput; |
29 | import org.qedeq.base.io.TextOutput; |
30 | import org.qedeq.base.trace.Trace; |
31 | import org.qedeq.base.utility.DateUtility; |
32 | import org.qedeq.base.utility.EqualsUtility; |
33 | import org.qedeq.base.utility.StringUtility; |
34 | import org.qedeq.kernel.bo.log.QedeqLog; |
35 | import org.qedeq.kernel.bo.module.InternalModuleServiceCall; |
36 | import org.qedeq.kernel.bo.module.KernelNodeBo; |
37 | import org.qedeq.kernel.bo.module.KernelQedeqBo; |
38 | import org.qedeq.kernel.bo.module.Reference; |
39 | import org.qedeq.kernel.bo.service.basis.ControlVisitor; |
40 | import org.qedeq.kernel.bo.service.basis.ModuleServicePluginExecutor; |
41 | import org.qedeq.kernel.se.base.list.Element; |
42 | import org.qedeq.kernel.se.base.list.ElementList; |
43 | import org.qedeq.kernel.se.base.module.Add; |
44 | import org.qedeq.kernel.se.base.module.Author; |
45 | import org.qedeq.kernel.se.base.module.AuthorList; |
46 | import org.qedeq.kernel.se.base.module.Axiom; |
47 | import org.qedeq.kernel.se.base.module.ChangedRule; |
48 | import org.qedeq.kernel.se.base.module.ChangedRuleList; |
49 | import org.qedeq.kernel.se.base.module.Chapter; |
50 | import org.qedeq.kernel.se.base.module.Conclusion; |
51 | import org.qedeq.kernel.se.base.module.ConditionalProof; |
52 | import org.qedeq.kernel.se.base.module.Existential; |
53 | import org.qedeq.kernel.se.base.module.FormalProof; |
54 | import org.qedeq.kernel.se.base.module.FormalProofLine; |
55 | import org.qedeq.kernel.se.base.module.FormalProofLineList; |
56 | import org.qedeq.kernel.se.base.module.FunctionDefinition; |
57 | import org.qedeq.kernel.se.base.module.Header; |
58 | import org.qedeq.kernel.se.base.module.Hypothesis; |
59 | import org.qedeq.kernel.se.base.module.Import; |
60 | import org.qedeq.kernel.se.base.module.ImportList; |
61 | import org.qedeq.kernel.se.base.module.InitialFunctionDefinition; |
62 | import org.qedeq.kernel.se.base.module.InitialPredicateDefinition; |
63 | import org.qedeq.kernel.se.base.module.Latex; |
64 | import org.qedeq.kernel.se.base.module.LatexList; |
65 | import org.qedeq.kernel.se.base.module.LinkList; |
66 | import org.qedeq.kernel.se.base.module.LiteratureItem; |
67 | import org.qedeq.kernel.se.base.module.LiteratureItemList; |
68 | import org.qedeq.kernel.se.base.module.LocationList; |
69 | import org.qedeq.kernel.se.base.module.ModusPonens; |
70 | import org.qedeq.kernel.se.base.module.Node; |
71 | import org.qedeq.kernel.se.base.module.PredicateDefinition; |
72 | import org.qedeq.kernel.se.base.module.Proof; |
73 | import org.qedeq.kernel.se.base.module.Proposition; |
74 | import org.qedeq.kernel.se.base.module.Qedeq; |
75 | import org.qedeq.kernel.se.base.module.Rename; |
76 | import org.qedeq.kernel.se.base.module.Rule; |
77 | import org.qedeq.kernel.se.base.module.Section; |
78 | import org.qedeq.kernel.se.base.module.SectionList; |
79 | import org.qedeq.kernel.se.base.module.Specification; |
80 | import org.qedeq.kernel.se.base.module.Subsection; |
81 | import org.qedeq.kernel.se.base.module.SubsectionList; |
82 | import org.qedeq.kernel.se.base.module.SubsectionType; |
83 | import org.qedeq.kernel.se.base.module.SubstFree; |
84 | import org.qedeq.kernel.se.base.module.SubstFunc; |
85 | import org.qedeq.kernel.se.base.module.SubstPred; |
86 | import org.qedeq.kernel.se.base.module.Universal; |
87 | import org.qedeq.kernel.se.base.module.UsedByList; |
88 | import org.qedeq.kernel.se.common.ModuleAddress; |
89 | import org.qedeq.kernel.se.common.ModuleContext; |
90 | import org.qedeq.kernel.se.common.ModuleDataException; |
91 | import org.qedeq.kernel.se.common.ModuleService; |
92 | import org.qedeq.kernel.se.common.RuleKey; |
93 | import org.qedeq.kernel.se.common.SourceFileExceptionList; |
94 | |
95 | |
96 | /** |
97 | * Transfer a QEDEQ module into a LaTeX file. |
98 | * <p> |
99 | * <b>This is just a quick written generator. No parsing or validation |
100 | * of inline LaTeX text is done. This class just generates some LaTeX output to be able to |
101 | * get a visual impression of a QEDEQ module.</b> |
102 | * |
103 | * @author Michael Meyling |
104 | */ |
105 | public final class Qedeq2LatexExecutor extends ControlVisitor implements ModuleServicePluginExecutor { |
106 | |
107 | /** This class. */ |
108 | private static final Class CLASS = Qedeq2LatexExecutor.class; |
109 | |
110 | // TODO m31 20100316: check number area for error codes |
111 | // TODO m31 20100803: add JUnit tests for all error codes |
112 | |
113 | /** Output goes here. */ |
114 | private TextOutput printer; |
115 | |
116 | /** Filter text to get and produce text in this language. */ |
117 | private String language; |
118 | |
119 | /** Filter for this detail level. */ |
120 | // private String level; |
121 | |
122 | /** Should additional information be put into LaTeX output? E.g. QEDEQ reference names. */ |
123 | private final boolean info; |
124 | |
125 | /** Should only names and formulas be be printed? */ |
126 | private final boolean brief; |
127 | |
128 | /** Current node id. */ |
129 | private String id; |
130 | |
131 | /** Current node title. */ |
132 | private String title; |
133 | |
134 | /** Sub context like "getIntroduction()". */ |
135 | private String subContext = ""; |
136 | |
137 | /** Remembered proof line label. */ |
138 | private String label = ""; |
139 | |
140 | /** Remembered proof line formula. */ |
141 | private String formula = ""; |
142 | |
143 | /** Remembered proof line reason. */ |
144 | private String reason = ""; |
145 | |
146 | /** Remembered proof line tabulator level. */ |
147 | private int tabLevel = 0; |
148 | |
149 | /** Alphabet for tagging. */ |
150 | private static final String ALPHABET = "abcdefghijklmnopqrstuvwxyz"; |
151 | |
152 | /** |
153 | * Constructor. |
154 | * |
155 | * @param plugin This plugin we work for. |
156 | * @param prop QEDEQ BO object. |
157 | * @param parameters Parameters. |
158 | */ |
159 | public Qedeq2LatexExecutor(final ModuleService plugin, final KernelQedeqBo prop, final Parameters parameters) { |
160 | super(plugin, prop); |
161 | info = parameters.getBoolean("info"); |
162 | brief = parameters.getBoolean("brief"); |
163 | } |
164 | |
165 | private ModuleService getPlugin() { |
166 | return (ModuleService) getService(); |
167 | } |
168 | |
169 | public Object executePlugin(final InternalModuleServiceCall call, final Object data) { |
170 | final String method = "executePlugin(QedeqBo, Map)"; |
171 | try { |
172 | QedeqLog.getInstance().logRequest("Generate LaTeX", getKernelQedeqBo().getUrl()); |
173 | final String[] languages = getKernelQedeqBo().getSupportedLanguages(); |
174 | for (int j = 0; j < languages.length; j++) { |
175 | language = languages[j]; |
176 | // level = "1"; |
177 | final String result = generateLatex(call, languages[j], "1").toString(); |
178 | if (languages[j] != null) { |
179 | QedeqLog.getInstance().logSuccessfulReply( |
180 | "LaTeX for language \"" + languages[j] |
181 | + "\" was generated from into \"" + result + "\"", getKernelQedeqBo().getUrl()); |
182 | } else { |
183 | QedeqLog.getInstance().logSuccessfulReply( |
184 | "LaTeX for default language " |
185 | + "was generated into \"" + result + "\"", getKernelQedeqBo().getUrl()); |
186 | } |
187 | } |
188 | if (languages.length == 0) { |
189 | QedeqLog.getInstance().logMessage("no supported language found, assuming 'en'"); |
190 | final String result = generateLatex(call, "en", "1").toString(); |
191 | QedeqLog.getInstance().logSuccessfulReply( |
192 | "LaTeX for language \"en" |
193 | + "\" was generated into \"" + result + "\"", getKernelQedeqBo().getUrl()); |
194 | } |
195 | } catch (final SourceFileExceptionList e) { |
196 | final String msg = "Generation failed"; |
197 | Trace.fatal(CLASS, this, method, msg, e); |
198 | QedeqLog.getInstance().logFailureReply(msg, getKernelQedeqBo().getUrl(), e.getMessage()); |
199 | } catch (IOException e) { |
200 | final String msg = "Generation failed"; |
201 | Trace.fatal(CLASS, this, method, msg, e); |
202 | QedeqLog.getInstance().logFailureReply(msg, getKernelQedeqBo().getUrl(), e.getMessage()); |
203 | } catch (final RuntimeException e) { |
204 | Trace.fatal(CLASS, this, method, "unexpected problem", e); |
205 | QedeqLog.getInstance().logFailureReply( |
206 | "Generation failed", getKernelQedeqBo().getUrl(), "unexpected problem: " |
207 | + (e.getMessage() != null ? e.getMessage() : e.toString())); |
208 | } |
209 | return null; |
210 | } |
211 | |
212 | /** |
213 | * Get an input stream for the LaTeX creation. |
214 | * |
215 | * @param call This process executes us. |
216 | * @param language Filter text to get and produce text in this language only. |
217 | * @param level Filter for this detail level. LATER mime 20050205: not supported |
218 | * yet. |
219 | * @return Resulting LaTeX. |
220 | * @throws SourceFileExceptionList Major problem occurred. |
221 | * @throws IOException File IO failed. |
222 | */ |
223 | public InputStream createLatex(final InternalModuleServiceCall call, final String language, final String level) |
224 | throws SourceFileExceptionList, IOException { |
225 | return new FileInputStream(generateLatex(call, language, level)); |
226 | } |
227 | |
228 | /** |
229 | * Gives a LaTeX representation of given QEDEQ module as InputStream. |
230 | * |
231 | * @param call This process executes us. |
232 | * @param language Filter text to get and produce text in this language only. |
233 | * <code>null</code> is ok. |
234 | * @param level Filter for this detail level. LATER mime 20050205: not supported |
235 | * yet. |
236 | * @return Resulting LaTeX. |
237 | * @throws SourceFileExceptionList Major problem occurred. |
238 | * @throws IOException File IO failed. |
239 | */ |
240 | public File generateLatex(final InternalModuleServiceCall call, final String language, final String level) |
241 | throws SourceFileExceptionList, IOException { |
242 | final String method = "generateLatex(String, String)"; |
243 | this.language = language; |
244 | // this.level = level; |
245 | // first we try to get more information about required modules and their predicates.. |
246 | try { |
247 | getServices().loadRequiredModules(call.getInternalServiceProcess(), getKernelQedeqBo()); |
248 | getServices().checkWellFormedness(call.getInternalServiceProcess(), getKernelQedeqBo()); |
249 | } catch (Exception e) { |
250 | // we continue and ignore external predicates |
251 | Trace.trace(CLASS, method, e); |
252 | } |
253 | String tex = getKernelQedeqBo().getModuleAddress().getFileName(); |
254 | if (tex.toLowerCase(Locale.US).endsWith(".xml")) { |
255 | tex = tex.substring(0, tex.length() - 4); |
256 | } |
257 | if (language != null && language.length() > 0) { |
258 | tex = tex + "_" + language; |
259 | } |
260 | // the destination is the configured destination directory plus the (relative) |
261 | // localized file (or path) name |
262 | File destination = new File(getServices().getConfig() |
263 | .getGenerationDirectory(), tex + ".tex").getCanonicalFile(); |
264 | |
265 | init(); |
266 | |
267 | try { |
268 | // TODO 20110204 m31: here we should choose the correct encoding; perhaps GUI configurable? |
269 | if ("de".equals(language)) { |
270 | printer = new TextOutput(getKernelQedeqBo().getName(), new FileOutputStream(destination), |
271 | "ISO-8859-1") { |
272 | public void append(final String txt) { |
273 | super.append(escapeUmlauts(txt)); |
274 | } |
275 | }; |
276 | } else { |
277 | printer = new TextOutput(getKernelQedeqBo().getName(), new FileOutputStream(destination), |
278 | "UTF-8") { |
279 | public void append(final String txt) { |
280 | super.append(escapeUmlauts(txt)); |
281 | } |
282 | }; |
283 | } |
284 | traverse(call.getInternalServiceProcess()); |
285 | } finally { |
286 | getKernelQedeqBo().addPluginErrorsAndWarnings(getPlugin(), getErrorList(), getWarningList()); |
287 | if (printer != null) { |
288 | printer.flush(); |
289 | printer.close(); |
290 | } |
291 | } |
292 | if (printer != null && printer.checkError()) { |
293 | throw printer.getError(); |
294 | } |
295 | try { |
296 | QedeqBoDuplicateLanguageChecker.check(call); |
297 | } catch (SourceFileExceptionList warnings) { |
298 | getKernelQedeqBo().addPluginErrorsAndWarnings(getPlugin(), null, warnings); |
299 | } |
300 | return destination.getCanonicalFile(); |
301 | } |
302 | |
303 | /** |
304 | * Reset counters and other variables. Should be executed before {@link #traverse()}. |
305 | */ |
306 | protected void init() { |
307 | id = null; |
308 | title = null; |
309 | subContext = ""; |
310 | } |
311 | |
312 | public final void visitEnter(final Qedeq qedeq) { |
313 | printer.println("% -*- TeX" |
314 | + (language != null ? ":" + language.toUpperCase(Locale.US) : "") + " -*-"); |
315 | printer.println("%%% ===================================================================="); |
316 | printer.println("%%% @LaTeX-file " + printer.getName()); |
317 | printer.println("%%% Generated from " + getKernelQedeqBo().getModuleAddress()); |
318 | printer.println("%%% Generated at " + DateUtility.getTimestamp()); |
319 | printer.println("%%% ===================================================================="); |
320 | printer.println(); |
321 | printer.println( |
322 | "%%% Permission is granted to copy, distribute and/or modify this document"); |
323 | printer.println("%%% under the terms of the GNU Free Documentation License, Version 1.2"); |
324 | printer.println("%%% or any later version published by the Free Software Foundation;"); |
325 | printer.println( |
326 | "%%% with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts."); |
327 | printer.println(); |
328 | printer.println("\\documentclass[a4paper,german,10pt,twoside]{book}"); |
329 | if ("de".equals(language)) { |
330 | printer.println("\\usepackage[german]{babel}"); |
331 | } else { |
332 | if (!"en".equals(language)) { |
333 | printer.println("%%% TODO unknown language: " + language); |
334 | } |
335 | printer.println("\\usepackage[english]{babel}"); |
336 | } |
337 | printer.println("\\usepackage{makeidx}"); |
338 | printer.println("\\usepackage{amsmath,amsthm,amssymb}"); |
339 | printer.println("\\usepackage{color}"); |
340 | printer.println("\\usepackage{xr}"); |
341 | printer.println("\\usepackage{tabularx}"); |
342 | // printer.println("\\usepackage{epsfig,longtable}"); |
343 | // printer.println("\\usepackage{ltabptch}"); // not installed on our server |
344 | printer.println("\\usepackage[bookmarks=true,bookmarksnumbered,bookmarksopen,"); |
345 | printer.println(" unicode=true,colorlinks=true,linkcolor=webgreen,"); |
346 | printer.println(" pagebackref=true,pdfnewwindow=true,pdfstartview=FitH]{hyperref}"); |
347 | printer.println("\\definecolor{webgreen}{rgb}{0,.5,0}"); |
348 | printer.println("\\usepackage{epsfig,longtable}"); |
349 | printer.println("\\usepackage{graphicx}"); |
350 | printer.println("\\usepackage[all]{hypcap}"); |
351 | printer.println(); |
352 | if ("de".equals(language)) { |
353 | // TODO m31 20100313: validate different counter types |
354 | // printer.println("\\newtheorem{thm}{Theorem}[chapter]"); |
355 | printer.println("\\newtheorem{thm}{Theorem}"); |
356 | printer.println("\\newtheorem{cor}[thm]{Korollar}"); |
357 | printer.println("\\newtheorem{lem}[thm]{Lemma}"); |
358 | printer.println("\\newtheorem{prop}[thm]{Proposition}"); |
359 | printer.println("\\newtheorem{ax}{Axiom}"); |
360 | printer.println("\\newtheorem{rul}{Regel}"); |
361 | printer.println(); |
362 | printer.println("\\theoremstyle{definition}"); |
363 | printer.println("\\newtheorem{defn}{Definition}"); |
364 | printer.println("\\newtheorem{idefn}[defn]{Initiale Definition}"); |
365 | printer.println(); |
366 | printer.println("\\theoremstyle{remark}"); |
367 | printer.println("\\newtheorem{rem}[thm]{Bemerkung}"); |
368 | printer.println("\\newtheorem*{notation}{Notation}"); |
369 | } else { |
370 | if (!"en".equals(language)) { |
371 | printer.println("%%% TODO unknown language: " + language); |
372 | } |
373 | // TODO m31 20100313: validate different counter types |
374 | // printer.println("\\newtheorem{thm}{Theorem}[chapter]"); |
375 | printer.println("\\newtheorem{thm}{Theorem}"); |
376 | printer.println("\\newtheorem{cor}[thm]{Corollary}"); |
377 | printer.println("\\newtheorem{lem}[thm]{Lemma}"); |
378 | printer.println("\\newtheorem{prop}[thm]{Proposition}"); |
379 | printer.println("\\newtheorem{ax}{Axiom}"); |
380 | printer.println("\\newtheorem{rul}{Rule}"); |
381 | printer.println(); |
382 | printer.println("\\theoremstyle{definition}"); |
383 | printer.println("\\newtheorem{defn}{Definition}"); |
384 | printer.println("\\newtheorem{idefn}[defn]{Initial Definition}"); |
385 | printer.println(); |
386 | printer.println("\\theoremstyle{remark}"); |
387 | printer.println("\\newtheorem{rem}[thm]{Remark}"); |
388 | printer.println("\\newtheorem*{notation}{Notation}"); |
389 | } |
390 | printer.println(); |
391 | printer.println(); |
392 | printer.println("\\addtolength{\\textheight}{7\\baselineskip}"); |
393 | printer.println("\\addtolength{\\topmargin}{-5\\baselineskip}"); |
394 | printer.println(); |
395 | printer.println("\\setlength{\\parindent}{0pt}"); |
396 | printer.println(); |
397 | printer.println("\\frenchspacing \\sloppy"); |
398 | printer.println(); |
399 | printer.println("\\makeindex"); |
400 | printer.println(); |
401 | printer.println(); |
402 | } |
403 | |
404 | public final void visitLeave(final Qedeq qedeq) { |
405 | printer.println("\\addcontentsline{toc}{chapter}{\\indexname} \\printindex"); |
406 | printer.println(); |
407 | printer.println("\\end{document}"); |
408 | printer.println(); |
409 | } |
410 | |
411 | public void visitEnter(final Header header) { |
412 | final LatexList tit = header.getTitle(); |
413 | printer.print("\\title{"); |
414 | printer.print(getLatexListEntry("getTitle()", tit)); |
415 | printer.println("}"); |
416 | printer.println("\\author{"); |
417 | final AuthorList authors = getKernelQedeqBo().getQedeq().getHeader().getAuthorList(); |
418 | final StringBuffer authorList = new StringBuffer(); |
419 | for (int i = 0; i < authors.size(); i++) { |
420 | if (i > 0) { |
421 | authorList.append(", "); |
422 | printer.println(", "); |
423 | } |
424 | final Author author = authors.get(i); |
425 | final String name = author.getName().getLatex().trim(); |
426 | printer.print(name); |
427 | authorList.append(name); |
428 | String email = author.getEmail(); |
429 | if (email != null && email.trim().length() > 0) { |
430 | authorList.append(" \\href{mailto:" + email + "}{" + email + "}"); |
431 | } |
432 | } |
433 | printer.println(); |
434 | printer.println("}"); |
435 | printer.println(); |
436 | printer.println("\\begin{document}"); |
437 | printer.println(); |
438 | printer.println("\\maketitle"); |
439 | printer.println(); |
440 | printer.println("\\setlength{\\parskip}{5pt plus 2pt minus 1pt}"); |
441 | printer.println("\\mbox{}"); |
442 | printer.println("\\vfill"); |
443 | printer.println(); |
444 | final String url = getKernelQedeqBo().getUrl(); |
445 | if (url != null && url.length() > 0) { |
446 | printer.println("\\par"); |
447 | if ("de".equals(language)) { |
448 | printer.println("Die Quelle f{\"ur} dieses Dokument ist hier zu finden:"); |
449 | } else { |
450 | if (!"en".equals(language)) { |
451 | printer.println("%%% TODO unknown language: " + language); |
452 | } |
453 | printer.println("The source for this document can be found here:"); |
454 | } |
455 | printer.println("\\par"); |
456 | printer.println("\\url{" + url + "}"); |
457 | printer.println(); |
458 | } |
459 | { |
460 | printer.println("\\par"); |
461 | if ("de".equals(language)) { |
462 | printer.println("Die vorliegende Publikation ist urheberrechtlich gesch{\"u}tzt."); |
463 | } else { |
464 | if (!"en".equals(language)) { |
465 | printer.println("%%% TODO unknown language: " + language); |
466 | } |
467 | printer.println("Copyright by the authors. All rights reserved."); |
468 | } |
469 | } |
470 | final String email = header.getEmail(); |
471 | if (email != null && email.length() > 0) { |
472 | final String emailUrl = "\\href{mailto:" + email + "}{" + email + "}"; |
473 | printer.println("\\par"); |
474 | if ("de".equals(language)) { |
475 | printer.println("Bei Fragen, Anregungen oder Bitte um Aufnahme in die Liste der" |
476 | + " abh\u00e4ngigen Module schicken Sie bitte eine EMail an die Adresse " |
477 | + emailUrl); |
478 | printer.println(); |
479 | printer.println("\\par"); |
480 | printer.println("Die Autoren dieses Dokuments sind:"); |
481 | printer.println(authorList); |
482 | } else { |
483 | if (!"en".equals(language)) { |
484 | printer.println("%%% TODO unknown language: " + language); |
485 | } |
486 | printer.println("If you have any questions, suggestions or want to add something" |
487 | + " to the list of modules that use this one, please send an email to the" |
488 | + " address " + emailUrl); |
489 | printer.println(); |
490 | printer.println("\\par"); |
491 | printer.println("The authors of this document are:"); |
492 | printer.println(authorList); |
493 | } |
494 | printer.println(); |
495 | } |
496 | } |
497 | |
498 | public void visitLeave(final Header header) { |
499 | printer.println(); |
500 | printer.println(); |
501 | printer.println("\\setlength{\\parskip}{0pt}"); |
502 | printer.println("\\tableofcontents"); |
503 | printer.println(); |
504 | printer.println("\\setlength{\\parskip}{5pt plus 2pt minus 1pt}"); |
505 | printer.println(); |
506 | } |
507 | |
508 | public void visitEnter(final ImportList imports) throws ModuleDataException { |
509 | printer.println(); |
510 | printer.println(); |
511 | printer.println("\\par"); |
512 | if ("de".equals(language)) { |
513 | printer.println("Benutzte QEDEQ module:"); |
514 | } else { |
515 | if (!"en".equals(language)) { |
516 | printer.println("%%% TODO unknown language: " + language); |
517 | } |
518 | printer.println("Used other QEDEQ modules:"); |
519 | } |
520 | printer.println(); |
521 | printer.println("\\par"); |
522 | printer.println(); |
523 | } |
524 | |
525 | public void visitEnter(final Import imp) throws ModuleDataException { |
526 | printer.println(); |
527 | printer.println("\\par"); |
528 | printer.print("\\textbf{" + imp.getLabel() + "} "); |
529 | final Specification spec = imp.getSpecification(); |
530 | printer.print(getLatex(spec.getName())); |
531 | if (spec.getLocationList() != null && spec.getLocationList().size() > 0 |
532 | && spec.getLocationList().get(0).getLocation().length() > 0) { |
533 | printer.print(" "); |
534 | printer.print("\\url{" + getPdfLink((KernelQedeqBo) getKernelQedeqBo() |
535 | .getLabels().getReferences().getQedeqBo(imp.getLabel())) + "}"); |
536 | } |
537 | printer.println(); |
538 | } |
539 | |
540 | /** |
541 | * Get URL for QEDEQ XML module. |
542 | * |
543 | * @param address Current module address. |
544 | * @param specification Find URL for this location list. |
545 | * @return URL or <code>""</code> if none (valid?) was found. |
546 | */ |
547 | private String getUrl(final ModuleAddress address, final Specification specification) { |
548 | final LocationList list = specification.getLocationList(); |
549 | if (list == null || list.size() <= 0) { |
550 | return ""; |
551 | } |
552 | try { |
553 | return address.getModulePaths(specification)[0].getUrl(); |
554 | } catch (IOException e) { |
555 | return ""; |
556 | } |
557 | } |
558 | |
559 | public void visitEnter(final Chapter chapter) { |
560 | // check if we print only brief and test for non text subnodes |
561 | if (brief) { |
562 | boolean hasFormalContent = false; |
563 | do { |
564 | final SectionList sections = chapter.getSectionList(); |
565 | if (sections == null) { |
566 | break; |
567 | } |
568 | for (int i = 0; i < sections.size() && !hasFormalContent; i++) { |
569 | final Section section = sections.get(i); |
570 | if (section == null) { |
571 | continue; |
572 | } |
573 | final SubsectionList subSections = section.getSubsectionList(); |
574 | if (subSections == null) { |
575 | continue; |
576 | } |
577 | for (int j = 0; j < subSections.size(); j++) { |
578 | final SubsectionType subSection = subSections.get(j); |
579 | if (!(subSection instanceof Subsection)) { |
580 | hasFormalContent = true; |
581 | break; |
582 | } |
583 | } |
584 | } |
585 | } while (false); |
586 | if (!hasFormalContent) { |
587 | setBlocked(true); |
588 | return; |
589 | } |
590 | } |
591 | printer.print("\\chapter"); |
592 | if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) { |
593 | printer.print("*"); |
594 | } |
595 | printer.print("{"); |
596 | printer.print(getLatexListEntry("getTitle()", chapter.getTitle())); |
597 | final String chapterLabel = "chapter" + getCurrentNumbers().getAbsoluteChapterNumber(); |
598 | printer.println("} \\label{" + chapterLabel + "} \\hypertarget{" + chapterLabel + "}{}"); |
599 | if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) { |
600 | printer.println("\\addcontentsline{toc}{chapter}{" |
601 | + getLatexListEntry("getTitle()", chapter.getTitle()) + "}"); |
602 | } |
603 | printer.println(); |
604 | if (chapter.getIntroduction() != null && !brief) { |
605 | printer.println(getLatexListEntry("getIntroduction()", chapter.getIntroduction())); |
606 | printer.println(); |
607 | } |
608 | } |
609 | |
610 | public void visitLeave(final Chapter chapter) { |
611 | printer.println("%% end of chapter " + getLatexListEntry("getTitle()", chapter.getTitle())); |
612 | printer.println(); |
613 | setBlocked(false); |
614 | } |
615 | |
616 | public void visitLeave(final SectionList list) { |
617 | printer.println(); |
618 | } |
619 | |
620 | public void visitEnter(final Section section) { |
621 | // check if we print only brief and test for non text subnodes |
622 | if (brief) { |
623 | boolean hasFormalContent = false; |
624 | do { |
625 | final SubsectionList subSections = section.getSubsectionList(); |
626 | if (subSections == null) { |
627 | break; |
628 | } |
629 | for (int j = 0; j < subSections.size(); j++) { |
630 | final SubsectionType subSection = subSections.get(j); |
631 | if (!(subSection instanceof Subsection)) { |
632 | hasFormalContent = true; |
633 | break; |
634 | } |
635 | } |
636 | } while (false); |
637 | if (!hasFormalContent) { |
638 | setBlocked(true); |
639 | return; |
640 | } |
641 | } |
642 | printer.print("\\section"); |
643 | if (section.getNoNumber() != null && section.getNoNumber().booleanValue()) { |
644 | printer.print("*"); |
645 | } |
646 | printer.print("{"); |
647 | printer.print(getLatexListEntry("getTitle()", section.getTitle())); |
648 | final String chapterLabel = "chapter" + getCurrentNumbers().getAbsoluteChapterNumber() |
649 | + "_section" + getCurrentNumbers().getAbsoluteSectionNumber(); |
650 | printer.println("} \\label{" + chapterLabel + "} \\hypertarget{" + chapterLabel + "}{}"); |
651 | if (section.getIntroduction() != null && !brief) { |
652 | printer.println(getLatexListEntry("getIntroduction()", section.getIntroduction())); |
653 | printer.println(); |
654 | } |
655 | } |
656 | |
657 | public void visitLeave(final Section section) { |
658 | setBlocked(false); |
659 | } |
660 | |
661 | public void visitEnter(final Subsection subsection) { |
662 | /* LATER mime 20070131: use this information? |
663 | if (subsection.getId() != null) { |
664 | printer.print(" id=\"" + subsection.getId() + "\""); |
665 | } |
666 | if (subsection.getLevel() != null) { |
667 | printer.print(" level=\"" + subsection.getLevel() + "\""); |
668 | } |
669 | */ |
670 | if (brief) { |
671 | return; |
672 | } |
673 | if (subsection.getTitle() != null) { |
674 | printer.print("\\subsection{"); |
675 | printer.println(getLatexListEntry("getTitle()", subsection.getTitle())); |
676 | printer.println("}"); |
677 | } |
678 | if (subsection.getId() != null) { |
679 | printer.println("\\label{" + subsection.getId() + "} \\hypertarget{" |
680 | + subsection.getId() + "}{}"); |
681 | } |
682 | printer.println(getLatexListEntry("getLatex()", subsection.getLatex())); |
683 | } |
684 | |
685 | public void visitLeave(final Subsection subsection) { |
686 | if (brief) { |
687 | return; |
688 | } |
689 | printer.println(); |
690 | printer.println(); |
691 | } |
692 | |
693 | public void visitEnter(final Node node) { |
694 | /** TODO mime 20070131: level filter |
695 | if (node.getLevel() != null) { |
696 | printer.print(" level=\"" + node.getLevel() + "\""); |
697 | } |
698 | */ |
699 | if (node.getPrecedingText() != null && !brief) { |
700 | printer.println("\\par"); |
701 | printer.println(getLatexListEntry("getPrecedingText()", node.getPrecedingText())); |
702 | printer.println(); |
703 | } |
704 | id = node.getId(); |
705 | title = null; |
706 | if (node.getTitle() != null) { |
707 | title = getLatexListEntry("getTitle()", node.getTitle()); |
708 | } |
709 | } |
710 | |
711 | public void visitLeave(final Node node) { |
712 | printer.println(); |
713 | if (node.getSucceedingText() != null && !brief) { |
714 | printer.println(getLatexListEntry("getSucceedingText()", node.getSucceedingText())); |
715 | printer.println(); |
716 | } |
717 | printer.println(); |
718 | } |
719 | |
720 | public void visitEnter(final Axiom axiom) { |
721 | printer.println("\\begin{ax}" + (title != null ? "[" + title + "]" : "")); |
722 | printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}"); |
723 | if (info) { |
724 | printer.println("{\\tt \\tiny [\\verb]" + id + "]]}"); |
725 | } |
726 | printFormula(axiom.getFormula().getElement()); |
727 | printer.println(getLatexListEntry("getDescription()", axiom.getDescription())); |
728 | printer.println("\\end{ax}"); |
729 | } |
730 | |
731 | public void visitEnter(final Proposition proposition) { |
732 | printer.println("\\begin{prop}" + (title != null ? "[" + title + "]" : "")); |
733 | printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}"); |
734 | if (info) { |
735 | printer.println("{\\tt \\tiny [\\verb]" + id + "]]}"); |
736 | } |
737 | printTopFormula(proposition.getFormula().getElement(), id); |
738 | printer.println(getLatexListEntry("getDescription()", proposition.getDescription())); |
739 | printer.println("\\end{prop}"); |
740 | } |
741 | |
742 | public void visitEnter(final Proof proof) { |
743 | /* LATER mime 20070131: filter level and kind |
744 | if (proof.getKind() != null) { |
745 | printer.print(" kind=\"" + proof.getKind() + "\""); |
746 | } |
747 | if (proof.getLevel() != null) { |
748 | printer.print(" level=\"" + proof.getLevel() + "\""); |
749 | } |
750 | */ |
751 | if (brief) { |
752 | setBlocked(true); |
753 | return; |
754 | } |
755 | printer.println("\\begin{proof}"); |
756 | printer.println(getLatexListEntry("getNonFormalProof()", proof.getNonFormalProof())); |
757 | printer.println("\\end{proof}"); |
758 | } |
759 | |
760 | public void visitLeave(final Proof proof) { |
761 | setBlocked(false); |
762 | } |
763 | |
764 | public void visitEnter(final FormalProof proof) { |
765 | if (brief) { |
766 | setBlocked(true); |
767 | return; |
768 | } |
769 | tabLevel = 0; |
770 | printer.println("\\begin{proof}"); |
771 | // if ("de".equals(language)) { |
772 | // printer.println("Beweis (formal):"); |
773 | // } else { |
774 | // printer.println("Proof (formal):"); |
775 | // } |
776 | } |
777 | |
778 | public void visitEnter(final FormalProofLineList lines) { |
779 | if (tabLevel == 0) { |
780 | printer.println("\\mbox{}\\\\"); |
781 | printer.println("\\begin{longtable}[h!]{r@{\\extracolsep{\\fill}}p{9cm}@{\\extracolsep{\\fill}}p{4cm}}"); |
782 | } |
783 | } |
784 | |
785 | public void visitLeave(final FormalProofLineList lines) { |
786 | if (tabLevel == 0) { |
787 | printer.println(" & & \\qedhere"); |
788 | printer.println("\\end{longtable}"); |
789 | } |
790 | } |
791 | |
792 | public void visitEnter(final FormalProofLine line) { |
793 | if (line.getLabel() != null) { |
794 | label = line.getLabel(); |
795 | } else { |
796 | label = ""; |
797 | } |
798 | if (line.getFormula() != null) { |
799 | formula = "$" + getKernelQedeqBo().getElement2Latex().getLatex(line.getFormula().getElement()) + "$"; |
800 | } else { |
801 | formula = ""; |
802 | } |
803 | if (line.getReason() != null) { |
804 | reason = line.getReason().toString(); |
805 | } else { |
806 | reason = ""; |
807 | } |
808 | } |
809 | |
810 | public void visitLeave(final FormalProofLine line) { |
811 | if (brief) { |
812 | return; |
813 | } |
814 | linePrintln(); |
815 | } |
816 | |
817 | /** |
818 | * Print proof line made out of label, formula and reason. |
819 | */ |
820 | private void linePrintln() { |
821 | if (formula.length() == 0 && reason.length() == 0) { |
822 | return; |
823 | } |
824 | if (label.length() > 0) { |
825 | String display = getNodeBo().getNodeVo().getId() + "!" + label; |
826 | printer.print("\\label{" + display + "} \\hypertarget{" + display |
827 | + "}{\\mbox{(" + label + ")}} "); |
828 | } |
829 | printer.print(" \\ & \\ "); |
830 | for (int i = 0; i < tabLevel; i++) { |
831 | printer.print("\\mbox{\\qquad}"); |
832 | } |
833 | if (formula.length() > 0) { |
834 | printer.print(formula); |
835 | } |
836 | printer.print(" \\ & \\ "); |
837 | if (reason.length() > 0) { |
838 | printer.print("{\\tiny "); |
839 | printer.print(reason); |
840 | printer.print("}"); |
841 | } |
842 | printer.println(" \\\\ "); |
843 | reason = ""; |
844 | formula = ""; |
845 | label = ""; |
846 | } |
847 | |
848 | private String getReference(final String reference) { |
849 | return getReference(reference, "getReference()"); |
850 | } |
851 | |
852 | private String getReference(final String reference, final String subContext) { |
853 | final String context = getCurrentContext().getLocationWithinModule(); |
854 | try { |
855 | getCurrentContext().setLocationWithinModule(context + "." + subContext); |
856 | return (getReference(reference, null, null)); |
857 | } finally { |
858 | getCurrentContext().setLocationWithinModule(context); |
859 | } |
860 | } |
861 | |
862 | public void visitEnter(final ModusPonens r) throws ModuleDataException { |
863 | if (brief) { |
864 | return; |
865 | } |
866 | reason = getRuleReference(r.getName()); |
867 | boolean one = false; |
868 | if (r.getReference1() != null) { |
869 | reason += " " + getReference(r.getReference1(), "getReference1()"); |
870 | one = true; |
871 | } |
872 | if (r.getReference1() != null) { |
873 | if (one) { |
874 | reason += ","; |
875 | } |
876 | reason += " " + getReference(r.getReference2(), "getReference2()"); |
877 | } |
878 | } |
879 | |
880 | public void visitEnter(final Add r) throws ModuleDataException { |
881 | if (brief) { |
882 | return; |
883 | } |
884 | reason = getRuleReference(r.getName()); |
885 | if (r.getReference() != null) { |
886 | reason += " " + getReference(r.getReference()); |
887 | } |
888 | } |
889 | |
890 | public void visitEnter(final Rename r) throws ModuleDataException { |
891 | if (brief) { |
892 | return; |
893 | } |
894 | reason = getRuleReference(r.getName()); |
895 | if (r.getOriginalSubjectVariable() != null) { |
896 | reason += " $" + getKernelQedeqBo().getElement2Latex().getLatex( |
897 | r.getOriginalSubjectVariable()) + "$"; |
898 | } |
899 | if (r.getReplacementSubjectVariable() != null) { |
900 | reason += " by $" + getKernelQedeqBo().getElement2Latex().getLatex( |
901 | r.getReplacementSubjectVariable()) + "$"; |
902 | } |
903 | if (r.getReference() != null) { |
904 | reason += " in " + getReference(r.getReference()); |
905 | } |
906 | } |
907 | |
908 | public void visitEnter(final SubstFree r) throws ModuleDataException { |
909 | if (brief) { |
910 | return; |
911 | } |
912 | reason = getRuleReference(r.getName()); |
913 | if (r.getSubjectVariable() != null) { |
914 | reason += " $" + getKernelQedeqBo().getElement2Latex().getLatex( |
915 | r.getSubjectVariable()) + "$"; |
916 | } |
917 | if (r.getSubstituteTerm() != null) { |
918 | reason += " by $" + getKernelQedeqBo().getElement2Latex().getLatex( |
919 | r.getSubstituteTerm()) + "$"; |
920 | } |
921 | if (r.getReference() != null) { |
922 | reason += " in " + getReference(r.getReference()); |
923 | } |
924 | } |
925 | |
926 | public void visitEnter(final SubstFunc r) throws ModuleDataException { |
927 | if (brief) { |
928 | return; |
929 | } |
930 | reason = getRuleReference(r.getName()); |
931 | if (r.getFunctionVariable() != null) { |
932 | reason += " $" + getKernelQedeqBo().getElement2Latex().getLatex( |
933 | r.getFunctionVariable()) + "$"; |
934 | } |
935 | if (r.getSubstituteTerm() != null) { |
936 | reason += " by $" + getKernelQedeqBo().getElement2Latex().getLatex( |
937 | r.getSubstituteTerm()) + "$"; |
938 | } |
939 | if (r.getReference() != null) { |
940 | reason += " in " + getReference(r.getReference()); |
941 | } |
942 | } |
943 | |
944 | public void visitEnter(final SubstPred r) throws ModuleDataException { |
945 | if (brief) { |
946 | return; |
947 | } |
948 | reason = getRuleReference(r.getName()); |
949 | if (r.getPredicateVariable() != null) { |
950 | reason += " $" + getKernelQedeqBo().getElement2Latex().getLatex( |
951 | r.getPredicateVariable()) + "$"; |
952 | } |
953 | if (r.getSubstituteFormula() != null) { |
954 | reason += " by $" + getKernelQedeqBo().getElement2Latex().getLatex( |
955 | r.getSubstituteFormula()) + "$"; |
956 | } |
957 | if (r.getReference() != null) { |
958 | reason += " in " + getReference(r.getReference()); |
959 | } |
960 | } |
961 | |
962 | public void visitEnter(final Existential r) throws ModuleDataException { |
963 | if (brief) { |
964 | return; |
965 | } |
966 | reason = getRuleReference(r.getName()); |
967 | if (r.getSubjectVariable() != null) { |
968 | reason += " with $" + getKernelQedeqBo().getElement2Latex().getLatex( |
969 | r.getSubjectVariable()) + "$"; |
970 | } |
971 | if (r.getReference() != null) { |
972 | reason += " in " + getReference(r.getReference()); |
973 | } |
974 | } |
975 | |
976 | public void visitEnter(final Universal r) throws ModuleDataException { |
977 | if (brief) { |
978 | return; |
979 | } |
980 | reason = getRuleReference(r.getName()); |
981 | if (r.getSubjectVariable() != null) { |
982 | reason += " with $" + getKernelQedeqBo().getElement2Latex().getLatex( |
983 | r.getSubjectVariable()) + "$"; |
984 | } |
985 | if (r.getReference() != null) { |
986 | reason += " in " + getReference(r.getReference()); |
987 | } |
988 | } |
989 | |
990 | public void visitEnter(final ConditionalProof r) throws ModuleDataException { |
991 | if (brief) { |
992 | return; |
993 | } |
994 | reason = getRuleReference(r.getName()); |
995 | printer.print(" \\ & \\ "); |
996 | for (int i = 0; i < tabLevel; i++) { |
997 | printer.print("\\mbox{\\qquad}"); |
998 | } |
999 | printer.println("Conditional Proof"); |
1000 | printer.print(" \\ & \\ "); |
1001 | printer.println(" \\\\ "); |
1002 | tabLevel++; |
1003 | } |
1004 | |
1005 | public void visitLeave(final ConditionalProof proof) { |
1006 | if (brief) { |
1007 | return; |
1008 | } |
1009 | tabLevel--; |
1010 | } |
1011 | |
1012 | public void visitEnter(final Hypothesis hypothesis) { |
1013 | if (brief) { |
1014 | return; |
1015 | } |
1016 | reason = "Hypothesis"; |
1017 | if (hypothesis.getLabel() != null) { |
1018 | label = hypothesis.getLabel(); |
1019 | } |
1020 | if (hypothesis.getFormula() != null) { |
1021 | formula = "$" + getKernelQedeqBo().getElement2Latex().getLatex( |
1022 | hypothesis.getFormula().getElement()) + "$"; |
1023 | } |
1024 | } |
1025 | |
1026 | public void visitLeave(final Hypothesis hypothesis) { |
1027 | if (brief) { |
1028 | return; |
1029 | } |
1030 | linePrintln(); |
1031 | } |
1032 | |
1033 | public void visitEnter(final Conclusion conclusion) { |
1034 | if (brief) { |
1035 | return; |
1036 | } |
1037 | tabLevel--; |
1038 | reason = "Conclusion"; |
1039 | if (conclusion.getLabel() != null) { |
1040 | label = conclusion.getLabel(); |
1041 | } |
1042 | if (conclusion.getFormula() != null) { |
1043 | formula = "$" + getKernelQedeqBo().getElement2Latex().getLatex( |
1044 | conclusion.getFormula().getElement()) + "$"; |
1045 | } |
1046 | } |
1047 | |
1048 | public void visitLeave(final Conclusion conclusion) { |
1049 | if (brief) { |
1050 | return; |
1051 | } |
1052 | linePrintln(); |
1053 | tabLevel++; |
1054 | } |
1055 | |
1056 | public void visitLeave(final FormalProof proof) { |
1057 | if (!getBlocked()) { |
1058 | printer.println("\\end{proof}"); |
1059 | } |
1060 | setBlocked(false); |
1061 | } |
1062 | |
1063 | public void visitEnter(final InitialPredicateDefinition definition) { |
1064 | printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : "")); |
1065 | printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}"); |
1066 | if (info) { |
1067 | printer.println("{\\tt \\tiny [\\verb]" + id + "]]}"); |
1068 | } |
1069 | printer.print("$$"); |
1070 | printer.println(getLatex(definition.getPredCon())); |
1071 | printer.println("$$"); |
1072 | printer.println(getLatexListEntry("getDescription()", definition.getDescription())); |
1073 | printer.println("\\end{idefn}"); |
1074 | } |
1075 | |
1076 | public void visitEnter(final PredicateDefinition definition) { |
1077 | printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : "")); |
1078 | printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}"); |
1079 | if (info) { |
1080 | printer.println("{\\tt \\tiny [\\verb]" + id + "]]}"); |
1081 | } |
1082 | printer.print("$$"); |
1083 | printer.print(getLatex(definition.getFormula().getElement())); |
1084 | printer.println("$$"); |
1085 | printer.println(getLatexListEntry("getDescription()", definition.getDescription())); |
1086 | printer.println("\\end{defn}"); |
1087 | } |
1088 | |
1089 | public void visitEnter(final InitialFunctionDefinition definition) { |
1090 | printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : "")); |
1091 | printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}"); |
1092 | if (info) { |
1093 | printer.println("{\\tt \\tiny [\\verb]" + id + "]]}"); |
1094 | } |
1095 | printer.print("$$"); |
1096 | printer.print(getLatex(definition.getFunCon())); |
1097 | printer.println("$$"); |
1098 | printer.println(getLatexListEntry("getDescription()", definition.getDescription())); |
1099 | printer.println("\\end{defn}"); |
1100 | } |
1101 | |
1102 | public void visitEnter(final FunctionDefinition definition) { |
1103 | printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : "")); |
1104 | printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}"); |
1105 | if (info) { |
1106 | printer.println("{\\tt \\tiny [\\verb]" + id + "]]}"); |
1107 | } |
1108 | printer.print("$$"); |
1109 | printer.print(getLatex(definition.getFormula().getElement())); |
1110 | printer.println("$$"); |
1111 | printer.println("\\end{defn}"); |
1112 | } |
1113 | |
1114 | public void visitLeave(final FunctionDefinition definition) { |
1115 | // nothing to do |
1116 | } |
1117 | |
1118 | public void visitEnter(final Rule rule) { |
1119 | printer.println("\\begin{rul}" + (title != null ? "[" + title + "]" : "")); |
1120 | printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}"); |
1121 | if (info) { |
1122 | printer.println("{\\tt \\tiny [\\verb]" + id + "]]}"); |
1123 | } |
1124 | printer.println(); |
1125 | printer.println("\\par"); |
1126 | printer.println("{\\em " |
1127 | + (rule.getName() != null ? " Name: \\verb]" + rule.getName() + "]" : "") |
1128 | + (rule.getVersion() != null ? " - Version: \\verb]" + rule.getVersion() + "]" : "") |
1129 | + "}"); |
1130 | printer.println(); |
1131 | printer.println(); |
1132 | printer.println(getLatexListEntry("getDescription()", rule.getDescription())); |
1133 | printer.println("\\end{rul}"); |
1134 | } |
1135 | |
1136 | public void visitLeave(final Rule rule) { |
1137 | // nothing to do |
1138 | } |
1139 | |
1140 | public void visitEnter(final LinkList linkList) { |
1141 | if (linkList.size() <= 0) { |
1142 | return; |
1143 | } |
1144 | if ("de".equals(language)) { |
1145 | printer.println("Basierend auf: "); |
1146 | } else { |
1147 | if (!"en".equals(language)) { |
1148 | printer.println("%%% TODO unknown language: " + language); |
1149 | } |
1150 | printer.println("Based on: "); |
1151 | } |
1152 | for (int i = 0; i < linkList.size(); i++) { |
1153 | if (linkList.get(i) != null) { |
1154 | printer.print(" " + getReference(linkList.get(i), "get(" + i + ")")); |
1155 | } |
1156 | }; |
1157 | printer.println(); |
1158 | } |
1159 | |
1160 | public void visitEnter(final ChangedRuleList list) { |
1161 | if (list.size() <= 0) { |
1162 | return; |
1163 | } |
1164 | if ("de".equals(language)) { |
1165 | printer.println("Die folgenden Regeln m\u00fcssen erweitert werden."); |
1166 | } else { |
1167 | if (!"en".equals(language)) { |
1168 | printer.println("%%% TODO unknown language: " + language); |
1169 | } |
1170 | printer.println("The following rules have to be extended."); |
1171 | } |
1172 | printer.println(); |
1173 | } |
1174 | |
1175 | public void visitEnter(final ChangedRule rule) { |
1176 | printer.println("\\par"); |
1177 | printer.println("\\label{" + id + "!" + rule.getName() + "} \\hypertarget{" + id + "!" |
1178 | + rule.getName() + "}{}"); |
1179 | printer.print("{\\em " |
1180 | + (rule.getName() != null ? " Name: \\verb]" + rule.getName() + "]" : "") |
1181 | + (rule.getVersion() != null ? " - Version: \\verb]" + rule.getVersion() + "]" : "")); |
1182 | RuleKey old = getLocalRuleKey(rule.getName()); |
1183 | if (old == null && getKernelQedeqBo().getExistenceChecker() != null) { |
1184 | old = getKernelQedeqBo().getExistenceChecker().getParentRuleKey(rule.getName()); |
1185 | } |
1186 | if (old != null) { |
1187 | printer.print(" - Old Version: " |
1188 | + getRuleReference(rule.getName(), old.getVersion())); |
1189 | } |
1190 | printer.println("}"); |
1191 | rule.getName(); |
1192 | printer.println(); |
1193 | if (rule.getDescription() != null) { |
1194 | printer.println(getLatexListEntry("getDescription()", rule.getDescription())); |
1195 | printer.println(); |
1196 | printer.println(); |
1197 | } |
1198 | } |
1199 | |
1200 | |
1201 | public void visitEnter(final LiteratureItemList list) { |
1202 | printer.println("\\backmatter"); |
1203 | printer.println(); |
1204 | printer.println("\\begin{thebibliography}{99}"); |
1205 | if ("de".equals(language)) { |
1206 | printer.println("\\addcontentsline{toc}{chapter}{Literaturverzeichnis}"); |
1207 | } else { |
1208 | if (!"en".equals(language)) { |
1209 | printer.println("%%% TODO unknown language: " + language); |
1210 | } |
1211 | printer.println("\\addcontentsline{toc}{chapter}{Bibliography}"); |
1212 | } |
1213 | final ImportList imports = getKernelQedeqBo().getQedeq().getHeader().getImportList(); |
1214 | if (imports != null && imports.size() > 0) { |
1215 | printer.println(); |
1216 | printer.println(); |
1217 | printer.println("%% Used other QEDEQ modules:"); |
1218 | for (int i = 0; i < imports.size(); i++) { |
1219 | final Import imp = imports.get(i); |
1220 | printer.print("\\bibitem{" + imp.getLabel() + "} "); |
1221 | final Specification spec = imp.getSpecification(); |
1222 | printer.print(getLatex(spec.getName())); |
1223 | if (spec.getLocationList() != null && spec.getLocationList().size() > 0 |
1224 | && spec.getLocationList().get(0).getLocation().length() > 0) { |
1225 | printer.print(" "); |
1226 | // TODO m31 20070205, 2010727: later on here must stand the location that was used |
1227 | // to verify the document contents. |
1228 | // Also get other informations like authors, title, etc. |
1229 | // It might also be better to link to URL? |
1230 | // printer.print("\\url{" + getUrl(getQedeqBo().getModuleAddress(), spec) + "}"); |
1231 | printer.print("\\url{" + getPdfLink((KernelQedeqBo) getKernelQedeqBo() |
1232 | .getLabels().getReferences().getQedeqBo(imp.getLabel())) + "}"); |
1233 | } |
1234 | printer.println(); |
1235 | } |
1236 | printer.println(); |
1237 | printer.println(); |
1238 | printer.println("%% Other references:"); |
1239 | printer.println(); |
1240 | } |
1241 | } |
1242 | |
1243 | public void visitLeave(final LiteratureItemList list) { |
1244 | final UsedByList usedby = getKernelQedeqBo().getQedeq().getHeader().getUsedByList(); |
1245 | if (usedby != null && usedby.size() > 0) { |
1246 | printer.println(); |
1247 | printer.println(); |
1248 | printer.println("%% QEDEQ modules that use this one:"); |
1249 | for (int i = 0; i < usedby.size(); i++) { |
1250 | final Specification spec = usedby.get(i); |
1251 | printer.print("\\bibitem{" + spec.getName() + "} "); |
1252 | printer.print(getLatex(spec.getName())); |
1253 | final String url = getUrl(getKernelQedeqBo().getModuleAddress(), spec); |
1254 | if (url != null && url.length() > 0) { |
1255 | printer.print(" "); |
1256 | printer.print("\\url{" + url + "}"); |
1257 | } |
1258 | printer.println(); |
1259 | } |
1260 | printer.println(); |
1261 | printer.println(); |
1262 | } |
1263 | printer.println("\\end{thebibliography}"); |
1264 | } |
1265 | |
1266 | public void visitEnter(final LiteratureItem item) { |
1267 | printer.print("\\bibitem{" + item.getLabel() + "} "); |
1268 | printer.println(getLatexListEntry("getItem()", item.getItem())); |
1269 | printer.println(); |
1270 | } |
1271 | |
1272 | /** |
1273 | * Print top level formula. If the formula has the form <code>AND(.., .., ..)</code> the |
1274 | * formula is broken down in several labeled lines. |
1275 | * |
1276 | * @param element Formula to print. |
1277 | * @param mainLabel Main formula label. |
1278 | */ |
1279 | private void printTopFormula(final Element element, final String mainLabel) { |
1280 | if (!element.isList() || !element.getList().getOperator().equals("AND")) { |
1281 | printFormula(element); |
1282 | return; |
1283 | } |
1284 | final ElementList list = element.getList(); |
1285 | printer.println("\\mbox{}"); |
1286 | printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{0.9\\linewidth}l}}"); |
1287 | for (int i = 0; i < list.size(); i++) { |
1288 | String newLabel = ""; |
1289 | if (list.size() >= ALPHABET.length() * ALPHABET.length()) { |
1290 | newLabel = "" + (i + 1); |
1291 | } else { |
1292 | // TODO 20110303 m31: this dosn't work if we have more than 26 * 26 elements |
1293 | if (list.size() > ALPHABET.length()) { |
1294 | final int div = (i / ALPHABET.length()); |
1295 | newLabel = "" + ALPHABET.charAt(div); |
1296 | } |
1297 | newLabel += ALPHABET.charAt(i % ALPHABET.length()); |
1298 | } |
1299 | // final String label = (i < ALPHABET.length() ? "" + ALPHABET .charAt(i) : "" + i); |
1300 | printer.println("\\centering $" + getLatex(list.getElement(i)) + "$" |
1301 | + " & \\label{" + mainLabel + "/" + newLabel + "} \\hypertarget{" + mainLabel + "/" |
1302 | + newLabel + "}{} \\mbox{\\emph{(" + newLabel + ")}} " |
1303 | + (i + 1 < list.size() ? "\\\\" : "")); |
1304 | } |
1305 | printer.println("\\end{longtable}"); |
1306 | } |
1307 | |
1308 | /** |
1309 | * Print formula. |
1310 | * |
1311 | * @param element Formula to print. |
1312 | */ |
1313 | private void printFormula(final Element element) { |
1314 | printer.println("\\mbox{}"); |
1315 | printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{\\linewidth}}}"); |
1316 | printer.println("\\centering $" + getLatex(element) + "$"); |
1317 | printer.println("\\end{longtable}"); |
1318 | } |
1319 | |
1320 | /** |
1321 | * Get LaTeX element presentation. |
1322 | * |
1323 | * @param element Print this element. |
1324 | * @return LaTeX form of element. |
1325 | */ |
1326 | private String getLatex(final Element element) { |
1327 | return getKernelQedeqBo().getElement2Latex().getLatex(element); |
1328 | } |
1329 | |
1330 | /** |
1331 | * Filters correct entry out of LaTeX list. Filter criterion is for example the correct |
1332 | * language. |
1333 | * TODO mime 20050205: filter level too? |
1334 | * |
1335 | * @param method This method was called. Used to get the correct sub context. |
1336 | * Should not be null. If it is empty the <code>subContext</code> |
1337 | * is not changed. |
1338 | * @param list List of LaTeX texts. |
1339 | * @return Filtered text. |
1340 | */ |
1341 | private String getLatexListEntry(final String method, final LatexList list) { |
1342 | if (list == null) { |
1343 | return ""; |
1344 | } |
1345 | if (method.length() > 0) { |
1346 | subContext = method; |
1347 | } |
1348 | try { |
1349 | for (int i = 0; language != null && i < list.size(); i++) { |
1350 | if (language.equals(list.get(i).getLanguage())) { |
1351 | if (method.length() > 0) { |
1352 | subContext = method + ".get(" + i + ")"; |
1353 | } |
1354 | return getLatex(list.get(i)); |
1355 | } |
1356 | } |
1357 | // OK, we didn't found the language, so we take the default language |
1358 | final String def = getKernelQedeqBo().getOriginalLanguage(); |
1359 | for (int i = 0; i < list.size(); i++) { |
1360 | if (EqualsUtility.equals(def, list.get(i).getLanguage())) { |
1361 | if (method.length() > 0) { |
1362 | subContext = method + ".get(" + i + ")"; |
1363 | } |
1364 | return "MISSING! OTHER: " + getLatex(list.get(i)); |
1365 | } |
1366 | } |
1367 | // OK, we didn't find wanted and default language, so we take the first non empty one |
1368 | for (int i = 0; i < list.size(); i++) { |
1369 | if (method.length() > 0) { |
1370 | subContext = method + ".get(" + i + ")"; |
1371 | } |
1372 | if (null != list.get(i) && null != list.get(i).getLatex() |
1373 | && list.get(i).getLatex().trim().length() > 0) { |
1374 | return "MISSING! OTHER: " + getLatex(list.get(i)); |
1375 | } |
1376 | } |
1377 | return "MISSING!"; |
1378 | } finally { |
1379 | if (method.length() > 0) { |
1380 | subContext = ""; |
1381 | } |
1382 | } |
1383 | } |
1384 | |
1385 | /** |
1386 | * Get really LaTeX. Does some simple character replacements for umlauts. Also transforms |
1387 | * <code>\qref{key}</code> into LaTeX. |
1388 | * |
1389 | * @param latex Unescaped text. |
1390 | * @return Really LaTeX. |
1391 | */ |
1392 | private String getLatex(final Latex latex) { |
1393 | if (latex == null || latex.getLatex() == null) { |
1394 | return ""; |
1395 | } |
1396 | StringBuffer result = new StringBuffer(latex.getLatex()); |
1397 | |
1398 | // LATER mime 20080324: check if LaTeX is correct and no forbidden tags are used |
1399 | |
1400 | transformQref(result); |
1401 | |
1402 | return deleteLineLeadingWhitespace(result.toString()); |
1403 | } |
1404 | |
1405 | /** |
1406 | * Transform <code>\qref{key}</code> entries into common LaTeX code. |
1407 | * |
1408 | * LATER mime 20080324: write JUnitTests to be sure that no runtime exceptions are thrown if |
1409 | * reference is at end of latex etc. |
1410 | * |
1411 | * @param result Work on this buffer. |
1412 | */ |
1413 | private void transformQref(final StringBuffer result) { |
1414 | final String method = "transformQref(StringBuffer)"; |
1415 | final StringBuffer buffer = new StringBuffer(result.toString()); |
1416 | final TextInput input = new TextInput(buffer); |
1417 | int last = 0; |
1418 | try { |
1419 | result.setLength(0); |
1420 | while (input.forward("\\qref{")) { |
1421 | final SourcePosition startPosition = input.getSourcePosition(); |
1422 | final int start = input.getPosition(); |
1423 | if (!input.forward("}")) { |
1424 | addWarning(LatexErrorCodes.QREF_END_NOT_FOUND_CODE, |
1425 | LatexErrorCodes.QREF_END_NOT_FOUND_TEXT, startPosition, |
1426 | input.getSourcePosition()); |
1427 | continue; |
1428 | } |
1429 | String ref = input.getSubstring(start + "\\qref{".length(), input.getPosition()).trim(); |
1430 | input.read(); // read } |
1431 | Trace.param(CLASS, this, method, "1 ref", ref); |
1432 | if (ref.length() == 0) { |
1433 | addWarning(LatexErrorCodes.QREF_EMPTY_CODE, LatexErrorCodes.QREF_EMPTY_TEXT, |
1434 | startPosition, input.getSourcePosition()); |
1435 | continue; |
1436 | } |
1437 | if (ref.length() > 1024) { |
1438 | addWarning(LatexErrorCodes.QREF_END_NOT_FOUND_CODE, |
1439 | LatexErrorCodes.QREF_END_NOT_FOUND_TEXT, startPosition, |
1440 | input.getSourcePosition()); |
1441 | continue; |
1442 | } |
1443 | if (ref.indexOf("{") >= 0) { |
1444 | addWarning(LatexErrorCodes.QREF_END_NOT_FOUND_CODE, |
1445 | LatexErrorCodes.QREF_END_NOT_FOUND_TEXT, startPosition, |
1446 | input.getSourcePosition()); |
1447 | continue; |
1448 | } |
1449 | final int end = input.getPosition(); |
1450 | final SourcePosition endPosition = input.getSourcePosition(); |
1451 | result.append(buffer.substring(last, start)); |
1452 | result.append(getReference(ref, startPosition, endPosition)); |
1453 | last = end; |
1454 | } |
1455 | } finally { // thanks to findbugs |
1456 | IoUtility.close(input); |
1457 | if (last < buffer.length()) { |
1458 | result.append(buffer.substring(last)); |
1459 | } |
1460 | } |
1461 | } |
1462 | |
1463 | private String getReference(final String reference, final SourcePosition start, final SourcePosition end) { |
1464 | final String method = "getReference(String, String)"; |
1465 | Trace.param(CLASS, this, method, "2 reference", reference); // qreference within module |
1466 | |
1467 | final Reference ref = getReference(reference, getCurrentContext(start, end), true, false); |
1468 | if (ref.isNodeLocalReference() && ref.isSubReference()) { |
1469 | return "\\hyperlink{" + ref.getNodeLabel() + "/" + ref.getSubLabel() + "}{" + "(" |
1470 | + ref.getSubLabel() + ")" + "}"; |
1471 | } |
1472 | |
1473 | if (ref.isNodeLocalReference() && ref.isProofLineReference()) { |
1474 | return "\\hyperlink{" + ref.getNodeLabel() + "!" + ref.getProofLineLabel() + "}{" + "(" |
1475 | + ref.getProofLineLabel() + ")" + "}"; |
1476 | } |
1477 | |
1478 | if (!ref.isExternal()) { |
1479 | return "\\hyperlink{" + ref.getNodeLabel() |
1480 | + (ref.isSubReference() ? "/" + ref.getSubLabel() : "") |
1481 | + (ref.isProofLineReference() ? "!" + ref.getProofLineLabel() : "") |
1482 | + "}{" |
1483 | + getNodeDisplay(ref.getNodeLabel(), ref.getNode()) |
1484 | + (ref.isSubReference() ? " (" + ref.getSubLabel() + ")" : "") |
1485 | + (ref.isProofLineReference() ? " (" + ref.getProofLineLabel() + ")" : "") |
1486 | + "}"; |
1487 | } |
1488 | |
1489 | // do we have an external module reference without node? |
1490 | if (ref.isExternalModuleReference()) { |
1491 | return "\\url{" + getPdfLink(ref.getExternalQedeq()) + "}~\\cite{" |
1492 | + ref.getExternalQedeqLabel() + "}"; |
1493 | // if we want to show the text "description": \href{my_url}{description} |
1494 | } |
1495 | |
1496 | String external = getPdfLink(ref.getExternalQedeq()); |
1497 | if (external.startsWith("file://")) { |
1498 | external = "file:" + external.substring("file://".length()); |
1499 | } |
1500 | return "\\hyperref{" + external + "}{}{" |
1501 | + ref.getNodeLabel() |
1502 | + (ref.isSubReference() ? "/" + ref.getSubLabel() : "") |
1503 | + (ref.isProofLineReference() ? "!" + ref.getProofLineLabel() : "") |
1504 | + "}{" + getNodeDisplay(ref.getNodeLabel(), ref.getNode()) |
1505 | + (ref.isSubReference() ? " (" + ref.getSubLabel() + ")" : "") |
1506 | + (ref.isProofLineReference() ? " (" + ref.getProofLineLabel() + ")" : "") |
1507 | + "}~\\cite{" + ref.getExternalQedeqLabel() + "}"; |
1508 | } |
1509 | |
1510 | private String getNodeDisplay(final String label, final KernelNodeBo kNode) { |
1511 | return StringUtility.replace(getNodeDisplay(label, kNode, language), " ", "~"); |
1512 | } |
1513 | |
1514 | private String getRuleReference(final String ruleName) { |
1515 | return getRuleReference(ruleName, ruleName); |
1516 | } |
1517 | |
1518 | private String getRuleReference(final String ruleName, final String caption) { |
1519 | final String method = "getRuleReference(String, String)"; |
1520 | Trace.param(CLASS, this, method, "ruleName", ruleName); |
1521 | RuleKey key = getLocalRuleKey(ruleName); |
1522 | if (key == null && getKernelQedeqBo().getExistenceChecker() != null) { |
1523 | key = getKernelQedeqBo().getExistenceChecker().getParentRuleKey(ruleName); |
1524 | } |
1525 | if (key == null) { |
1526 | key = getKernelQedeqBo().getLabels().getRuleKey(ruleName); |
1527 | } |
1528 | KernelQedeqBo qedeq = getKernelQedeqBo(); |
1529 | if (getKernelQedeqBo().getExistenceChecker() != null) { |
1530 | qedeq = getKernelQedeqBo().getExistenceChecker().getQedeq(key); |
1531 | } |
1532 | String localRef = getKernelQedeqBo().getLabels().getRuleLabel(key); |
1533 | final String refRuleName = qedeq.getLabels().getRule(key).getName(); |
1534 | if (!ruleName.equals(refRuleName)) { |
1535 | localRef += "!" + ruleName; |
1536 | } |
1537 | qedeq.getLabels().getRule(key).getName(); |
1538 | boolean local = getKernelQedeqBo().equals(qedeq); |
1539 | if (local) { |
1540 | return "\\hyperlink{" + localRef + "}{" + caption + "}"; |
1541 | } |
1542 | String external = getPdfLink(qedeq); |
1543 | if (external.startsWith("file://")) { |
1544 | external = "file:" + external.substring("file://".length()); |
1545 | } |
1546 | return "\\hyperref{" + external + "}{}{" + caption + "}{" |
1547 | + localRef + "}"; |
1548 | } |
1549 | |
1550 | /** |
1551 | * Get current module context. Uses sub context information. |
1552 | * |
1553 | * @param startDelta Skip position (relative to location start). Could be |
1554 | * <code>null</code>. |
1555 | * @param endDelta Mark until this column (relative to location start). |
1556 | * be <code>null</code> |
1557 | * @return Current module context. |
1558 | */ |
1559 | public ModuleContext getCurrentContext(final SourcePosition startDelta, |
1560 | final SourcePosition endDelta) { |
1561 | if (subContext.length() == 0) { |
1562 | return super.getCurrentContext(); |
1563 | } |
1564 | final ModuleContext c = new ModuleContext(super.getCurrentContext().getModuleLocation(), |
1565 | super.getCurrentContext().getLocationWithinModule() + "." + subContext, |
1566 | startDelta, endDelta); |
1567 | return c; |
1568 | } |
1569 | |
1570 | // TODO 20110214 m31: decide about removal |
1571 | // public ModuleContext getCurrentContext() { |
1572 | // throw new IllegalStateException("programming error"); |
1573 | // } |
1574 | |
1575 | |
1576 | /** |
1577 | * Add warning. |
1578 | * |
1579 | * @param code Warning code. |
1580 | * @param msg Warning message. |
1581 | * @param startDelta Skip position (relative to location start). Could be |
1582 | * <code>null</code>. |
1583 | * @param endDelta Mark until this column (relative to location start). |
1584 | * be <code>null</code> |
1585 | */ |
1586 | private void addWarning(final int code, final String msg, final SourcePosition startDelta, |
1587 | final SourcePosition endDelta) { |
1588 | Trace.param(CLASS, this, "addWarning", "msg", msg); |
1589 | addWarning(new LatexContentException(code, msg, getCurrentContext(startDelta, endDelta))); |
1590 | } |
1591 | |
1592 | /** |
1593 | * Get URL to for PDF version of module. If the referenced module doesn't |
1594 | * support the current language we switch to the original language. |
1595 | * |
1596 | * @param prop Get URL for this QEDEQ module. |
1597 | * @return URL to PDF. |
1598 | */ |
1599 | private String getPdfLink(final KernelQedeqBo prop) { |
1600 | if (prop == null) { |
1601 | return ""; |
1602 | } |
1603 | final String url = prop.getUrl(); |
1604 | final int dot = url.lastIndexOf("."); |
1605 | if (prop.isSupportedLanguage(language)) { |
1606 | return url.substring(0, dot) + "_" + language + ".pdf"; |
1607 | } |
1608 | final String a = prop.getOriginalLanguage(); |
1609 | return url.substring(0, dot) + (a.length() > 0 ? "_" + a : "") + ".pdf"; |
1610 | } |
1611 | |
1612 | /** |
1613 | * Get LaTeX from string. Escapes common characters. |
1614 | * Also gets rid of leading spaces if they are equal among the lines. |
1615 | * |
1616 | * @param text Unescaped text. |
1617 | * @return LaTeX. |
1618 | */ |
1619 | private String getLatex(final String text) { |
1620 | final StringBuffer buffer = new StringBuffer(text); |
1621 | StringUtility.replace(buffer, "\\", "\\textbackslash"); |
1622 | StringUtility.replace(buffer, "$", "\\$"); |
1623 | StringUtility.replace(buffer, "&", "\\&"); |
1624 | StringUtility.replace(buffer, "%", "\\%"); |
1625 | StringUtility.replace(buffer, "#", "\\#"); |
1626 | StringUtility.replace(buffer, "_", "\\_"); |
1627 | StringUtility.replace(buffer, "{", "\\{"); |
1628 | StringUtility.replace(buffer, "}", "\\}"); |
1629 | StringUtility.replace(buffer, "~", "\\textasciitilde"); |
1630 | StringUtility.replace(buffer, "^", "\\textasciicircum"); |
1631 | StringUtility.replace(buffer, "<", "\\textless"); |
1632 | StringUtility.replace(buffer, ">", "\\textgreater"); |
1633 | StringUtility.deleteLineLeadingWhitespace(buffer); |
1634 | return buffer.toString().trim(); |
1635 | } |
1636 | |
1637 | /** |
1638 | * Trims text. Also gets rid of leading spaces if they are equal among the lines. |
1639 | * |
1640 | * @param text Text. |
1641 | * @return Untrimed text. |
1642 | */ |
1643 | private String deleteLineLeadingWhitespace(final String text) { |
1644 | final StringBuffer buffer = new StringBuffer(text); |
1645 | StringUtility.deleteLineLeadingWhitespace(buffer); |
1646 | return buffer.toString().trim(); |
1647 | } |
1648 | |
1649 | /** |
1650 | * Get really LaTeX. Does some simple character replacements for umlauts. |
1651 | * LATER mime 20050205: filter more than German umlauts |
1652 | * |
1653 | * @param nearlyLatex Unescaped text. |
1654 | * @return Really LaTeX. |
1655 | */ |
1656 | private String escapeUmlauts(final String nearlyLatex) { |
1657 | if (nearlyLatex == null) { |
1658 | return ""; |
1659 | } |
1660 | final StringBuffer buffer = new StringBuffer(nearlyLatex); |
1661 | // System.out.println("before"); |
1662 | // System.out.println(buffer); |
1663 | // System.out.println(); |
1664 | // System.out.println("after"); |
1665 | // System.out.println(buffer); |
1666 | // System.out.println("*******************************************************************"); |
1667 | StringUtility.replace(buffer, "\u00fc", "{\\\"u}"); |
1668 | StringUtility.replace(buffer, "\u00f6", "{\\\"o}"); |
1669 | StringUtility.replace(buffer, "\u00e4", "{\\\"a}"); |
1670 | StringUtility.replace(buffer, "\u00dc", "{\\\"U}"); |
1671 | StringUtility.replace(buffer, "\u00d6", "{\\\"O}"); |
1672 | StringUtility.replace(buffer, "\u00c4", "{\\\"A}"); |
1673 | StringUtility.replace(buffer, "\u00df", "{\\ss}"); |
1674 | return buffer.toString(); |
1675 | } |
1676 | |
1677 | } |