1
2
3
4
5
6
7
8
9
10
11
12
13
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
98
99
100
101
102
103
104
105 public final class Qedeq2LatexExecutor extends ControlVisitor implements ModuleServicePluginExecutor {
106
107
108 private static final Class CLASS = Qedeq2LatexExecutor.class;
109
110
111
112
113
114 private TextOutput printer;
115
116
117 private String language;
118
119
120
121
122
123 private final boolean info;
124
125
126 private final boolean brief;
127
128
129 private String id;
130
131
132 private String title;
133
134
135 private String subContext = "";
136
137
138 private String label = "";
139
140
141 private String formula = "";
142
143
144 private String reason = "";
145
146
147 private int tabLevel = 0;
148
149
150 private static final String ALPHABET = "abcdefghijklmnopqrstuvwxyz";
151
152
153
154
155
156
157
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
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
214
215
216
217
218
219
220
221
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
230
231
232
233
234
235
236
237
238
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
245
246 try {
247 getServices().loadRequiredModules(call.getInternalServiceProcess(), getKernelQedeqBo());
248 getServices().checkWellFormedness(call.getInternalServiceProcess(), getKernelQedeqBo());
249 } catch (Exception e) {
250
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
261
262 File destination = new File(getServices().getConfig()
263 .getGenerationDirectory(), tex + ".tex").getCanonicalFile();
264
265 init();
266
267 try {
268
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
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
343
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
354
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
374
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
542
543
544
545
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
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
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
663
664
665
666
667
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
695
696
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
744
745
746
747
748
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
772
773
774
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
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
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
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
1227
1228
1229
1230
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
1274
1275
1276
1277
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
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
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
1310
1311
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
1322
1323
1324
1325
1326 private String getLatex(final Element element) {
1327 return getKernelQedeqBo().getElement2Latex().getLatex(element);
1328 }
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
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
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
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
1387
1388
1389
1390
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
1399
1400 transformQref(result);
1401
1402 return deleteLineLeadingWhitespace(result.toString());
1403 }
1404
1405
1406
1407
1408
1409
1410
1411
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();
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 {
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);
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
1490 if (ref.isExternalModuleReference()) {
1491 return "\\url{" + getPdfLink(ref.getExternalQedeq()) + "}~\\cite{"
1492 + ref.getExternalQedeqLabel() + "}";
1493
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
1552
1553
1554
1555
1556
1557
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
1571
1572
1573
1574
1575
1576
1577
1578
1579
1580
1581
1582
1583
1584
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
1594
1595
1596
1597
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
1614
1615
1616
1617
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
1639
1640
1641
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
1651
1652
1653
1654
1655
1656 private String escapeUmlauts(final String nearlyLatex) {
1657 if (nearlyLatex == null) {
1658 return "";
1659 }
1660 final StringBuffer buffer = new StringBuffer(nearlyLatex);
1661
1662
1663
1664
1665
1666
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 }