1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16 package org.qedeq.kernel.bo.service.unicode;
17
18 import java.io.IOException;
19 import java.util.ArrayList;
20 import java.util.List;
21
22 import org.apache.commons.lang.ArrayUtils;
23 import org.qedeq.base.io.AbstractOutput;
24 import org.qedeq.base.io.SourcePosition;
25 import org.qedeq.base.io.TextOutput;
26 import org.qedeq.base.trace.Trace;
27 import org.qedeq.base.utility.DateUtility;
28 import org.qedeq.base.utility.EqualsUtility;
29 import org.qedeq.base.utility.StringUtility;
30 import org.qedeq.kernel.bo.module.InternalServiceJob;
31 import org.qedeq.kernel.bo.module.KernelNodeBo;
32 import org.qedeq.kernel.bo.module.KernelQedeqBo;
33 import org.qedeq.kernel.bo.module.Reference;
34 import org.qedeq.kernel.bo.service.basis.ControlVisitor;
35 import org.qedeq.kernel.se.base.list.Element;
36 import org.qedeq.kernel.se.base.list.ElementList;
37 import org.qedeq.kernel.se.base.module.Add;
38 import org.qedeq.kernel.se.base.module.Author;
39 import org.qedeq.kernel.se.base.module.AuthorList;
40 import org.qedeq.kernel.se.base.module.Axiom;
41 import org.qedeq.kernel.se.base.module.ChangedRule;
42 import org.qedeq.kernel.se.base.module.ChangedRuleList;
43 import org.qedeq.kernel.se.base.module.Chapter;
44 import org.qedeq.kernel.se.base.module.Conclusion;
45 import org.qedeq.kernel.se.base.module.ConditionalProof;
46 import org.qedeq.kernel.se.base.module.Existential;
47 import org.qedeq.kernel.se.base.module.FormalProof;
48 import org.qedeq.kernel.se.base.module.FormalProofLine;
49 import org.qedeq.kernel.se.base.module.Formula;
50 import org.qedeq.kernel.se.base.module.FunctionDefinition;
51 import org.qedeq.kernel.se.base.module.Header;
52 import org.qedeq.kernel.se.base.module.Hypothesis;
53 import org.qedeq.kernel.se.base.module.Import;
54 import org.qedeq.kernel.se.base.module.ImportList;
55 import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
56 import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
57 import org.qedeq.kernel.se.base.module.Latex;
58 import org.qedeq.kernel.se.base.module.LatexList;
59 import org.qedeq.kernel.se.base.module.LinkList;
60 import org.qedeq.kernel.se.base.module.LiteratureItem;
61 import org.qedeq.kernel.se.base.module.LiteratureItemList;
62 import org.qedeq.kernel.se.base.module.LocationList;
63 import org.qedeq.kernel.se.base.module.ModusPonens;
64 import org.qedeq.kernel.se.base.module.Node;
65 import org.qedeq.kernel.se.base.module.PredicateDefinition;
66 import org.qedeq.kernel.se.base.module.Proof;
67 import org.qedeq.kernel.se.base.module.Proposition;
68 import org.qedeq.kernel.se.base.module.Qedeq;
69 import org.qedeq.kernel.se.base.module.Rename;
70 import org.qedeq.kernel.se.base.module.Rule;
71 import org.qedeq.kernel.se.base.module.Section;
72 import org.qedeq.kernel.se.base.module.SectionList;
73 import org.qedeq.kernel.se.base.module.Specification;
74 import org.qedeq.kernel.se.base.module.Subsection;
75 import org.qedeq.kernel.se.base.module.SubsectionList;
76 import org.qedeq.kernel.se.base.module.SubsectionType;
77 import org.qedeq.kernel.se.base.module.SubstFree;
78 import org.qedeq.kernel.se.base.module.SubstFunc;
79 import org.qedeq.kernel.se.base.module.SubstPred;
80 import org.qedeq.kernel.se.base.module.Universal;
81 import org.qedeq.kernel.se.base.module.UsedByList;
82 import org.qedeq.kernel.se.common.ModuleAddress;
83 import org.qedeq.kernel.se.common.ModuleContext;
84 import org.qedeq.kernel.se.common.ModuleDataException;
85 import org.qedeq.kernel.se.common.ModuleService;
86 import org.qedeq.kernel.se.common.SourceFileExceptionList;
87 import org.qedeq.kernel.se.visitor.QedeqNumbers;
88
89
90
91
92
93
94
95
96
97
98 public class Qedeq2UnicodeVisitor extends ControlVisitor implements ReferenceFinder {
99
100
101 private static final Class CLASS = Qedeq2UnicodeVisitor.class;
102
103
104 private AbstractOutput printer;
105
106
107 private String language;
108
109
110
111
112
113 private final boolean info;
114
115
116 private String id;
117
118
119 private String title;
120
121
122 private String subContext = "";
123
124
125 private int maxColumns;
126
127
128 private boolean addWarnings;
129
130
131 private final boolean brief;
132
133
134 private static final String ALPHABET = "abcdefghijklmnopqrstuvwxyz";
135
136
137 private ProofLineData lineData = new ProofLineData();
138
139
140 private int formulaWidth = 60;
141
142
143 private int reasonWidth = 35;
144
145
146 private String tab = "";
147
148
149
150
151
152
153
154
155
156
157
158
159
160 public Qedeq2UnicodeVisitor(final ModuleService plugin, final KernelQedeqBo prop,
161 final boolean info, final int maximumColumn, final boolean addWarnings,
162 final boolean brief) {
163 super(plugin, prop);
164 this.info = info;
165 this.maxColumns = maximumColumn;
166 this.addWarnings = addWarnings;
167 this.brief = brief;
168 }
169
170
171
172
173
174
175
176
177
178
179
180
181 public void generateUtf8(final InternalServiceJob process, final AbstractOutput printer,
182 final String language, final String level) throws SourceFileExceptionList, IOException {
183 setParameters(printer, language);
184 try {
185 traverse(process);
186 } finally {
187 getKernelQedeqBo().addPluginErrorsAndWarnings((ModuleService) getService(), getErrorList(),
188 getWarningList());
189 }
190 }
191
192
193
194
195
196
197
198 public void setParameters(final AbstractOutput printer,
199 final String language) {
200 this.printer = printer;
201 this.printer.setColumns(maxColumns);
202
203 if (maxColumns <= 0) {
204 formulaWidth = 80;
205 reasonWidth = 50;
206 } else if (maxColumns <= 50) {
207 this.printer.setColumns(50);
208 formulaWidth = 21;
209 reasonWidth = 21;
210 } else if (maxColumns <= 100) {
211 formulaWidth = (maxColumns - 8) * 50 / 100;
212 reasonWidth = (maxColumns - 8) * 50 / 100;
213 } else if (maxColumns <= 120) {
214 reasonWidth = 46 + (maxColumns - 100) / 5;
215 formulaWidth = maxColumns - 8 - reasonWidth;
216 } else {
217 reasonWidth = 50 + (maxColumns - 120) / 10;
218 formulaWidth = maxColumns - 8 - reasonWidth;
219 }
220
221
222
223 if (language == null) {
224 this.language = "en";
225 } else {
226 this.language = language;
227 }
228
229
230
231
232
233
234 init();
235 }
236
237
238
239
240 protected void init() {
241 id = null;
242 title = null;
243 subContext = "";
244 }
245
246 public final void visitEnter(final Qedeq qedeq) {
247 if (printer instanceof TextOutput) {
248 printer.println("================================================================================");
249 printer.println("UTF-8-file " + ((TextOutput) printer).getName());
250 printer.println("Generated from " + getKernelQedeqBo().getModuleAddress());
251 printer.println("Generated at " + DateUtility.getTimestamp());
252 printer.println("================================================================================");
253 printer.println();
254 printer.println("If the characters of this document don't display correctly try opening this");
255 printer.println("document within a webbrowser and if necessary change the encoding to");
256 printer.println("Unicode (UTF-8)");
257 printer.println();
258 printer.println("Permission is granted to copy, distribute and/or modify this document");
259 printer.println("under the terms of the GNU Free Documentation License, Version 1.2");
260 printer.println("or any later version published by the Free Software Foundation;");
261 printer.println("with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts.");
262 printer.println();
263 printer.println();
264 printer.println();
265 }
266 }
267
268 public final void visitLeave(final Qedeq qedeq) {
269 printer.println();
270 }
271
272 public void visitEnter(final Header header) {
273 final LatexList tit = header.getTitle();
274 underlineBig(getLatexListEntry("getTitle()", tit));
275 printer.println();
276 final AuthorList authors = getKernelQedeqBo().getQedeq().getHeader().getAuthorList();
277 final StringBuffer authorList = new StringBuffer();
278 for (int i = 0; i < authors.size(); i++) {
279 if (i > 0) {
280 authorList.append(" \n");
281 printer.println(", ");
282 }
283 final Author author = authors.get(i);
284 final String name = author.getName().getLatex().trim();
285 printer.print(name);
286 authorList.append(" " + name);
287 String email = author.getEmail();
288 if (email != null && email.trim().length() > 0) {
289 authorList.append(" <" + email + ">");
290 }
291 }
292 printer.println();
293 printer.println();
294 final String url = getKernelQedeqBo().getUrl();
295 if (url != null && url.length() > 0) {
296 printer.println();
297 if ("de".equals(language)) {
298 printer.println("Die Quelle f\u00FCr dieses Dokument ist hier zu finden:");
299 } else {
300 if (!"en".equals(language)) {
301 printer.println("%%% TODO unknown language: " + language);
302 }
303 printer.println("The source for this document can be found here:");
304 }
305 printer.println();
306 printer.println(url);
307 printer.println();
308 }
309 {
310 printer.println();
311 if ("de".equals(language)) {
312 printer.println("Die vorliegende Publikation ist urheberrechtlich gesch\u00FCtzt.");
313 } else {
314 if (!"en".equals(language)) {
315 printer.println("%%% TODO unknown language: " + language);
316 }
317 printer.println("Copyright by the authors. All rights reserved.");
318 }
319 }
320 final String email = header.getEmail();
321 if (email != null && email.length() > 0) {
322 printer.println();
323 printer.println();
324 if ("de".equals(language)) {
325 printer.println("Bei Fragen, Anregungen oder Bitte um Aufnahme in die Liste der"
326 + " abh\u00E4ngigen Module schicken Sie bitte eine EMail an die Adresse "
327 + email);
328 printer.println();
329 printer.println();
330 printer.println("Die Autoren dieses Dokuments sind:");
331 printer.println();
332 printer.println(authorList);
333 } else {
334 if (!"en".equals(language)) {
335 printer.println("%%% TODO unknown language: " + language);
336 }
337 printer.println("If you have any questions, suggestions or want to add something"
338 + " to the list of modules that use this one, please send an email to the"
339 + " address " + email);
340 printer.println();
341 printer.println();
342 printer.println("The authors of this document are:");
343 printer.println(authorList);
344 }
345 printer.println();
346 }
347 printer.println();
348 printer.println();
349 }
350
351 public void visitEnter(final ImportList imports) throws ModuleDataException {
352
353
354 printImports();
355 }
356
357
358
359
360
361
362
363
364 private String getUrl(final ModuleAddress address, final Specification specification) {
365 final LocationList list = specification.getLocationList();
366 if (list == null || list.size() <= 0) {
367 return "";
368 }
369 try {
370 return address.getModulePaths(specification)[0].getUrl();
371 } catch (IOException e) {
372 return "";
373 }
374 }
375
376 public void visitEnter(final Chapter chapter) {
377
378 if (brief) {
379 boolean hasFormalContent = false;
380 do {
381 final SectionList sections = chapter.getSectionList();
382 if (sections == null) {
383 break;
384 }
385 for (int i = 0; i < sections.size() && !hasFormalContent; i++) {
386 final Section section = sections.get(i);
387 if (section == null) {
388 continue;
389 }
390 final SubsectionList subSections = section.getSubsectionList();
391 if (subSections == null) {
392 continue;
393 }
394 for (int j = 0; j < subSections.size(); j++) {
395 final SubsectionType subSection = subSections.get(j);
396 if (!(subSection instanceof Subsection)) {
397 hasFormalContent = true;
398 break;
399 }
400 }
401 }
402 } while (false);
403 if (!hasFormalContent) {
404 setBlocked(true);
405 return;
406 }
407 }
408 final QedeqNumbers numbers = getCurrentNumbers();
409 if (numbers.isChapterNumbering()) {
410 if ("de".equals(language)) {
411 printer.println("Kapitel " + numbers.getChapterNumber() + " ");
412 } else {
413 printer.println("Chapter " + numbers.getChapterNumber() + " ");
414 }
415 printer.println();
416 printer.println();
417 }
418 underlineBig(getLatexListEntry("getTitle()", chapter.getTitle()));
419 printer.println();
420 if (chapter.getIntroduction() != null && !brief) {
421 printer.append(getLatexListEntry("getIntroduction()", chapter.getIntroduction()));
422 printer.println();
423 printer.println();
424 printer.println();
425 }
426 }
427
428 public void visitLeave(final Header header) {
429 printer.println();
430 printer.println("___________________________________________________");
431 printer.println();
432 printer.println();
433 }
434
435 public void visitLeave(final Chapter chapter) {
436 if (!getBlocked()) {
437 printer.println();
438 printer.println("___________________________________________________");
439 printer.println();
440 printer.println();
441 }
442 setBlocked(false);
443 }
444
445 public void visitEnter(final Section section) {
446
447 if (brief) {
448 boolean hasFormalContent = false;
449 do {
450 final SubsectionList subSections = section.getSubsectionList();
451 if (subSections == null) {
452 break;
453 }
454 for (int j = 0; j < subSections.size(); j++) {
455 final SubsectionType subSection = subSections.get(j);
456 if (!(subSection instanceof Subsection)) {
457 hasFormalContent = true;
458 break;
459 }
460 }
461 } while (false);
462 if (!hasFormalContent) {
463 setBlocked(true);
464 return;
465 }
466 }
467 final QedeqNumbers numbers = getCurrentNumbers();
468 final StringBuffer buffer = new StringBuffer();
469 if (numbers.isChapterNumbering()) {
470 buffer.append(numbers.getChapterNumber());
471 }
472 if (numbers.isSectionNumbering()) {
473 if (buffer.length() > 0) {
474 buffer.append(".");
475 }
476 buffer.append(numbers.getSectionNumber());
477 }
478 if (buffer.length() > 0 && section.getTitle() != null) {
479 buffer.append(" ");
480 }
481 buffer.append(getLatexListEntry("getTitle()", section.getTitle()));
482 underline(buffer.toString());
483 printer.println();
484 if (section.getIntroduction() != null && !brief) {
485 printer.append(getLatexListEntry("getIntroduction()", section.getIntroduction()));
486 printer.println();
487 printer.println();
488 printer.println();
489 }
490 }
491
492 public void visitLeave(final Section section) {
493 if (!getBlocked()) {
494 printer.println();
495 }
496 setBlocked(false);
497 }
498
499 public void visitEnter(final Subsection subsection) {
500 if (brief) {
501 return;
502 }
503 final QedeqNumbers numbers = getCurrentNumbers();
504 final StringBuffer buffer = new StringBuffer();
505 if (numbers.isChapterNumbering()) {
506 buffer.append(numbers.getChapterNumber());
507 }
508 if (numbers.isSectionNumbering()) {
509 if (buffer.length() > 0) {
510 buffer.append(".");
511 }
512 buffer.append(numbers.getSectionNumber());
513 }
514 if (buffer.length() > 0) {
515 buffer.append(".");
516 }
517 buffer.append(numbers.getSubsectionNumber());
518 if (buffer.length() > 0 && subsection.getTitle() != null) {
519 buffer.append(" ");
520 }
521 if (subsection.getTitle() != null) {
522 printer.print(buffer.toString());
523 printer.print(getLatexListEntry("getTitle()", subsection.getTitle()));
524 }
525 if (subsection.getId() != null && info) {
526 printer.print(" [" + subsection.getId() + "]");
527 }
528 if (subsection.getTitle() != null) {
529 printer.println();
530 printer.println();
531 }
532 printer.append(getLatexListEntry("getLatex()", subsection.getLatex()));
533 printer.println();
534 printer.println();
535 }
536
537 public void visitEnter(final Node node) {
538 if (node.getPrecedingText() != null && !brief) {
539 printer.append(getLatexListEntry("getPrecedingText()", node.getPrecedingText()));
540 printer.println();
541 printer.println();
542 }
543 id = node.getId();
544 title = null;
545 if (node.getTitle() != null) {
546 title = getLatexListEntry("getTitle()", node.getTitle());
547 }
548 }
549
550 public void visitLeave(final Node node) {
551 if (node.getSucceedingText() != null && !brief) {
552 printer.append(getLatexListEntry("getSucceedingText()", node.getSucceedingText()));
553 printer.println();
554 printer.println();
555 }
556 printer.println();
557 }
558
559 public void visitEnter(final Axiom axiom) {
560 final QedeqNumbers numbers = getCurrentNumbers();
561 printer.print("\u2609 ");
562 printer.print("Axiom " + numbers.getAxiomNumber());
563 printer.print(" ");
564 if (title != null && title.length() > 0) {
565 printer.print(" (" + title + ")");
566 }
567 if (info) {
568 printer.print(" [" + id + "]");
569 }
570 printer.println();
571 printer.println();
572 printer.print(" ");
573 printFormula(axiom.getFormula().getElement());
574 printer.println();
575 if (axiom.getDescription() != null) {
576 printer.append(getLatexListEntry("getDescription()", axiom.getDescription()));
577 printer.println();
578 printer.println();
579 }
580 }
581
582 public void visitEnter(final Proposition proposition) {
583 final QedeqNumbers numbers = getCurrentNumbers();
584 printer.print("\u2609 ");
585 printer.print("Proposition " + numbers.getPropositionNumber());
586 printer.print(" ");
587 if (title != null && title.length() > 0) {
588 printer.print(" (" + title + ")");
589 }
590 if (info) {
591 printer.print(" [" + id + "]");
592 }
593 printer.println();
594 printer.println();
595 printTopFormula(proposition.getFormula().getElement(), id);
596 printer.println();
597 if (proposition.getDescription() != null) {
598 printer.append(getLatexListEntry("getDescription()", proposition.getDescription()));
599 printer.println();
600 printer.println();
601 }
602 }
603
604 public void visitEnter(final Proof proof) {
605 if (brief) {
606 setBlocked(true);
607 return;
608 }
609 if ("de".equals(language)) {
610 printer.println("Beweis:");
611 } else {
612 printer.println("Proof:");
613 }
614 printer.append(getLatexListEntry("getNonFormalProof()", proof.getNonFormalProof()));
615 }
616
617 public void visitLeave(final Proof proof) {
618 printer.println();
619 printer.println("q.e.d.");
620 printer.println();
621 setBlocked(false);
622 }
623
624 public void visitEnter(final FormalProof proof) {
625 if (brief) {
626 setBlocked(true);
627 return;
628 }
629 if ("de".equals(language)) {
630 printer.println("Beweis (formal):");
631 } else {
632 printer.println("Proof (formal):");
633 }
634 }
635
636 public void visitLeave(final FormalProof proof) {
637 if (!brief) {
638 printer.println("q.e.d.");
639 printer.println();
640 }
641 setBlocked(false);
642 }
643
644
645 public void visitEnter(final FormalProofLine line) {
646 lineData.init();
647 if (line.getLabel() != null) {
648 lineData.setLineLabel(line.getLabel());
649 }
650 if (line.getReason() != null) {
651 setReason(line.getReason().toString());
652 }
653 setFormula(line.getFormula());
654 }
655
656 public void visitLeave(final FormalProofLine line) {
657 linePrintln();
658 }
659
660
661
662
663 private void linePrintln() {
664 if (!lineData.containsData()) {
665 return;
666 }
667 if (lineData.getLineLabel().length() > 0) {
668 printer.print(StringUtility.alignRight("(" + lineData.getLineLabel() + ")", 5) + " ");
669 }
670 for (int i = 0; i < lineData.lines(); i++) {
671 printer.skipToColumn(6);
672 printer.print(tab);
673 if (i < lineData.getFormula().length) {
674 printer.print(lineData.getFormula()[i]);
675 }
676 if (i < lineData.getReason().length) {
677 printer.skipToColumn(6 + 2 + formulaWidth);
678 printer.print(lineData.getReason()[i]);
679 }
680 printer.println();
681 }
682 lineData.init();
683 }
684
685 public void visitEnter(final ConditionalProof r) throws ModuleDataException {
686 lineData.init();
687 printer.skipToColumn(6);
688 printer.print(tab);
689 printer.println("Conditional Proof");
690 tab = tab + " ";
691 }
692
693 public void visitLeave(final ConditionalProof proof) {
694 tab = StringUtility.substring(tab, 0, tab.length() - 2);
695 }
696
697 public void visitEnter(final Hypothesis hypothesis) {
698 lineData.init();
699 if (hypothesis.getLabel() != null) {
700 lineData.setLineLabel(hypothesis.getLabel());
701 }
702 setReason("Hypothesis");
703 setFormula(hypothesis.getFormula());
704 }
705
706 public void visitLeave(final Hypothesis hypothesis) {
707 linePrintln();
708 }
709
710 public void visitEnter(final Conclusion conclusion) {
711 tab = StringUtility.substring(tab, 0, tab.length() - 2);
712 lineData.init();
713 if (conclusion.getLabel() != null) {
714 lineData.setLineLabel(conclusion.getLabel());
715 }
716 setReason("Conclusion");
717 setFormula(conclusion.getFormula());
718 linePrintln();
719 }
720
721 public void visitLeave(final Conclusion conclusion) {
722 linePrintln();
723 tab = tab + " ";
724 }
725
726 private void setReason(final String reasonString) {
727 final List list = new ArrayList();
728 int index = 0;
729 while (index < reasonString.length()) {
730 list.add(StringUtility.substring(reasonString, index, reasonWidth));
731 index += reasonWidth;
732 }
733 lineData.setReason((String[]) list.toArray(ArrayUtils.EMPTY_STRING_ARRAY));
734 }
735
736 private void setFormula(final Formula f) {
737 if (f != null && f.getElement() != null) {
738 lineData.setFormula(getUtf8(f.getElement(),
739 formulaWidth - tab.length()));
740 }
741 }
742
743 private String getReference(final String reference) {
744 return getReference(reference, "getReference()");
745 }
746
747 private String getReference(final String reference, final String subContext) {
748 final String context = getCurrentContext().getLocationWithinModule();
749 try {
750 getCurrentContext().setLocationWithinModule(context + "." + subContext);
751 return (getReferenceLink(reference, null, null));
752 } finally {
753 getCurrentContext().setLocationWithinModule(context);
754 }
755 }
756
757 public void visitEnter(final ModusPonens r) throws ModuleDataException {
758 String buffer = r.getName();
759 boolean one = false;
760 if (r.getReference1() != null) {
761 buffer += " " + getReference(r.getReference1(), "getReference1()");
762 one = true;
763 }
764 if (r.getReference1() != null) {
765 if (one) {
766 buffer += ",";
767 }
768 buffer += " " + getReference(r.getReference2(), "getReference2()");
769 }
770 setReason(buffer);
771 }
772
773 public void visitEnter(final Add r) throws ModuleDataException {
774 String buffer = r.getName();
775 if (r.getReference() != null) {
776 buffer += " " + getReference(r.getReference());
777 }
778 setReason(buffer);
779 }
780
781 public void visitEnter(final Rename r) throws ModuleDataException {
782 String buffer = r.getName();
783 if (r.getOriginalSubjectVariable() != null) {
784 buffer += " " + getUtf8(r.getOriginalSubjectVariable());
785 }
786 if (r.getReplacementSubjectVariable() != null) {
787 buffer += " by " + getUtf8(r.getReplacementSubjectVariable());
788 }
789 if (r.getReference() != null) {
790 buffer += " in " + getReference(r.getReference());
791 }
792 setReason(buffer);
793 }
794
795 public void visitEnter(final SubstFree r) throws ModuleDataException {
796 String buffer = r.getName();
797 if (r.getSubjectVariable() != null) {
798 buffer += " " + getUtf8(r.getSubjectVariable());
799 }
800 if (r.getSubstituteTerm() != null) {
801 buffer += " by " + getUtf8(r.getSubstituteTerm());
802 }
803 if (r.getReference() != null) {
804 buffer += " in " + getReference(r.getReference());
805 }
806 setReason(buffer);
807 }
808
809 public void visitEnter(final SubstFunc r) throws ModuleDataException {
810 String buffer = r.getName();
811 if (r.getFunctionVariable() != null) {
812 buffer += " " + getUtf8(r.getFunctionVariable());
813 }
814 if (r.getSubstituteTerm() != null) {
815 buffer += " by " + getUtf8(r.getSubstituteTerm());
816 }
817 if (r.getReference() != null) {
818 buffer += " in " + getReference(r.getReference());
819 }
820 setReason(buffer);
821 }
822
823 public void visitEnter(final SubstPred r) throws ModuleDataException {
824 String buffer = r.getName();
825 if (r.getPredicateVariable() != null) {
826 buffer += " " + getUtf8(r.getPredicateVariable());
827 }
828 if (r.getSubstituteFormula() != null) {
829 buffer += " by " + getUtf8(r.getSubstituteFormula());
830 }
831 if (r.getReference() != null) {
832 buffer += " in " + getReference(r.getReference());
833 }
834 setReason(buffer);
835 }
836
837 public void visitEnter(final Existential r) throws ModuleDataException {
838 String buffer = r.getName();
839 if (r.getSubjectVariable() != null) {
840 buffer += " with " + getUtf8(r.getSubjectVariable());
841 }
842 if (r.getReference() != null) {
843 buffer += " in " + getReference(r.getReference());
844 }
845 setReason(buffer);
846 }
847
848 public void visitEnter(final Universal r) throws ModuleDataException {
849 String buffer = r.getName();
850 if (r.getSubjectVariable() != null) {
851 buffer += " with " + getKernelQedeqBo().getElement2Utf8().getUtf8(
852 r.getSubjectVariable());
853 }
854 if (r.getReference() != null) {
855 buffer += " in " + getReference(r.getReference());
856 }
857 setReason(buffer);
858 }
859
860 public void visitEnter(final InitialPredicateDefinition definition) {
861 final QedeqNumbers numbers = getCurrentNumbers();
862 printer.print("\u2609 ");
863 final StringBuffer buffer = new StringBuffer();
864 if ("de".equals(language)) {
865 buffer.append("initiale ");
866 } else {
867 buffer.append("initial ");
868 }
869 buffer.append("Definition " + (numbers.getPredicateDefinitionNumber()
870 + numbers.getFunctionDefinitionNumber()));
871 printer.print(buffer.toString());
872 printer.print(" ");
873 if (title != null && title.length() > 0) {
874 printer.print(" (" + title + ")");
875 }
876 if (info) {
877 printer.print(" [" + id + "]");
878 }
879 printer.println();
880 printer.println();
881 printer.print(" ");
882 printer.println(getUtf8(definition.getPredCon()));
883 printer.println();
884 if (definition.getDescription() != null) {
885 printer.append(getLatexListEntry("getDescription()", definition.getDescription()));
886 printer.println();
887 printer.println();
888 }
889 }
890
891 public void visitEnter(final PredicateDefinition definition) {
892 final QedeqNumbers numbers = getCurrentNumbers();
893 printer.print("\u2609 ");
894 final StringBuffer buffer = new StringBuffer();
895 buffer.append("Definition " + (numbers.getPredicateDefinitionNumber()
896 + numbers.getFunctionDefinitionNumber()));
897 printer.print(buffer.toString());
898 printer.print(" ");
899 if (title != null && title.length() > 0) {
900 printer.print(" (" + title + ")");
901 }
902 if (info) {
903 printer.print(" [" + id + "]");
904 }
905 printer.println();
906 printer.println();
907 printer.print(" ");
908 printer.println(getUtf8(definition.getFormula().getElement()));
909 printer.println();
910 if (definition.getDescription() != null) {
911 printer.append(getLatexListEntry("getDescription()", definition.getDescription()));
912 printer.println();
913 printer.println();
914 }
915 }
916
917 public void visitEnter(final InitialFunctionDefinition definition) {
918 final QedeqNumbers numbers = getCurrentNumbers();
919 printer.print("\u2609 ");
920 final StringBuffer buffer = new StringBuffer();
921 if ("de".equals(language)) {
922 buffer.append("initiale ");
923 } else {
924 buffer.append("initial ");
925 }
926 buffer.append("Definition " + (numbers.getPredicateDefinitionNumber()
927 + numbers.getFunctionDefinitionNumber()));
928 printer.print(buffer.toString());
929 printer.print(" ");
930 if (title != null && title.length() > 0) {
931 printer.print(" (" + title + ")");
932 }
933 if (info) {
934 printer.print(" [" + id + "]");
935 }
936 printer.println();
937 printer.println();
938 printer.print(" ");
939 printer.println(getUtf8(definition.getFunCon()));
940 printer.println();
941 if (definition.getDescription() != null) {
942 printer.println(getLatexListEntry("getDescription()", definition.getDescription()));
943 printer.println();
944 }
945 }
946
947 public void visitEnter(final FunctionDefinition definition) {
948 final QedeqNumbers numbers = getCurrentNumbers();
949 printer.print("\u2609 ");
950 final StringBuffer buffer = new StringBuffer();
951 buffer.append("Definition " + (numbers.getPredicateDefinitionNumber()
952 + numbers.getFunctionDefinitionNumber()));
953 printer.print(buffer.toString());
954 printer.print(" ");
955 if (title != null && title.length() > 0) {
956 printer.print(" (" + title + ")");
957 }
958 if (info) {
959 printer.print(" [" + id + "]");
960 }
961 printer.println();
962 printer.println();
963 printer.print(" ");
964 printer.println(getUtf8(definition.getFormula().getElement()));
965 printer.println();
966 if (definition.getDescription() != null) {
967 printer.println(getLatexListEntry("getDescription()", definition.getDescription()));
968 printer.println();
969 }
970 }
971
972 public void visitEnter(final Rule rule) {
973 final QedeqNumbers numbers = getCurrentNumbers();
974 printer.print("\u2609 ");
975 if ("de".equals(language)) {
976 printer.print("Regel");
977 } else {
978 printer.print("Rule");
979 }
980 printer.print(" " + numbers.getRuleNumber());
981 printer.print(" ");
982 if (title != null && title.length() > 0) {
983 printer.print(" (" + title + ")");
984 }
985 if (info) {
986 printer.print(" [" + id + "]");
987 }
988 printer.println();
989 printer.println((rule.getName() != null ? " Name: " + rule.getName() : "")
990 + (rule.getVersion() != null ? " - Version: " + rule.getVersion() : ""));
991 printer.println();
992 if (rule.getDescription() != null) {
993 printer.append(getLatexListEntry("getDescription()", rule.getDescription()));
994 printer.println();
995 printer.println();
996 }
997 }
998
999 public void visitEnter(final LinkList linkList) {
1000 if (linkList.size() <= 0) {
1001 return;
1002 }
1003 if ("de".equals(language)) {
1004 printer.println("Basierend auf: ");
1005 } else {
1006 if (!"en".equals(language)) {
1007 printer.println("%%% TODO unknown language: " + language);
1008 }
1009 printer.println("Based on: ");
1010 }
1011 for (int i = 0; i < linkList.size(); i++) {
1012 if (linkList.get(i) != null) {
1013 printer.print(" (" + linkList.get(i) + ")");
1014 }
1015 };
1016 printer.println();
1017 }
1018
1019 public void visitEnter(final ChangedRuleList list) {
1020 if (list.size() <= 0) {
1021 return;
1022 }
1023 printer.println();
1024 if ("de".equals(language)) {
1025 printer.println("Die folgenden Regeln m\u00FCssen erweitert werden.");
1026 } else {
1027 if (!"en".equals(language)) {
1028 printer.println("%%% TODO unknown language: " + language);
1029 }
1030 printer.println("The following rules have to be extended.");
1031 }
1032 printer.println();
1033 }
1034
1035 public void visitEnter(final ChangedRule rule) {
1036 printer.println((rule.getName() != null ? " Name: " + rule.getName() : "")
1037 + (rule.getVersion() != null ? " - Version: " + rule.getVersion() : ""));
1038 printer.println();
1039 if (rule.getDescription() != null) {
1040 printer.append(getLatexListEntry("getDescription()", rule.getDescription()));
1041 printer.println();
1042 printer.println();
1043 }
1044
1045 }
1046
1047 public void visitEnter(final LiteratureItemList list) {
1048 printer.println();
1049 printer.println();
1050 if ("de".equals(language)) {
1051 underlineBig("Literaturverzeichnis");
1052 } else {
1053 underlineBig("Bibliography");
1054 }
1055 printImports();
1056 }
1057
1058
1059
1060
1061 private void printImports() {
1062 final ImportList imports = getKernelQedeqBo().getQedeq().getHeader().getImportList();
1063 if (imports != null && imports.size() > 0) {
1064 printer.println();
1065 printer.println();
1066 if ("de".equals(language)) {
1067 printer.println("Benutzte andere QEDEQ-Module:");
1068 } else {
1069 printer.println("Used other QEDEQ modules:");
1070 }
1071 printer.println();
1072 for (int i = 0; i < imports.size(); i++) {
1073 final Import imp = imports.get(i);
1074 printer.print("[" + imp.getLabel() + "] ");
1075 final Specification spec = imp.getSpecification();
1076 printer.print(spec.getName());
1077 if (spec.getLocationList() != null && spec.getLocationList().size() > 0
1078 && spec.getLocationList().get(0).getLocation().length() > 0) {
1079 printer.print(" ");
1080 printer.print(getUrl(getKernelQedeqBo().getModuleAddress(), spec));
1081 }
1082 printer.println();
1083 }
1084 printer.println();
1085 printer.println();
1086 }
1087 }
1088
1089 public void visitLeave(final LiteratureItemList list) {
1090 final UsedByList usedby = getKernelQedeqBo().getQedeq().getHeader().getUsedByList();
1091 if (usedby != null && usedby.size() > 0) {
1092 printer.println();
1093 printer.println();
1094 if ("de".equals(language)) {
1095 printer.println("QEDEQ-Module, welche dieses hier verwenden:");
1096 } else {
1097 printer.println("QEDEQ modules that use this one:");
1098 }
1099 for (int i = 0; i < usedby.size(); i++) {
1100 final Specification spec = usedby.get(i);
1101 printer.print(spec.getName());
1102 final String url = getUrl(getKernelQedeqBo().getModuleAddress(), spec);
1103 if (url != null && url.length() > 0) {
1104 printer.print(" ");
1105 printer.print(url);
1106 }
1107 printer.println();
1108 }
1109 printer.println();
1110 printer.println();
1111 }
1112 printer.println();
1113 }
1114
1115 public void visitEnter(final LiteratureItem item) {
1116 printer.print("[" + item.getLabel() + "] ");
1117 printer.println(getLatexListEntry("getItem()", item.getItem()));
1118 printer.println();
1119 }
1120
1121
1122
1123
1124
1125
1126
1127
1128 private void printTopFormula(final Element element, final String mainLabel) {
1129 if (!element.isList() || !element.getList().getOperator().equals("AND")) {
1130 printer.print(" ");
1131 printFormula(element);
1132 return;
1133 }
1134 final ElementList list = element.getList();
1135 for (int i = 0; i < list.size(); i++) {
1136 String label = "";
1137 if (list.size() >= ALPHABET.length() * ALPHABET.length()) {
1138 label = "" + (i + 1);
1139 } else {
1140 if (list.size() > ALPHABET.length()) {
1141 final int div = (i / ALPHABET.length());
1142 label = "" + ALPHABET.charAt(div);
1143 }
1144 label += ALPHABET.charAt(i % ALPHABET.length());
1145 }
1146 printer.println(" (" + label + ") " + getUtf8(list.getElement(i)));
1147 }
1148 }
1149
1150
1151
1152
1153
1154
1155 private void printFormula(final Element element) {
1156 printer.println(getUtf8(element));
1157 }
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169 private String getLatexListEntry(final String method, final LatexList list) {
1170 if (list == null) {
1171 return "";
1172 }
1173 if (method.length() > 0) {
1174 subContext = method;
1175 }
1176 try {
1177 for (int i = 0; i < list.size(); i++) {
1178 if (language.equals(list.get(i).getLanguage())) {
1179 if (method.length() > 0) {
1180 subContext = method + ".get(" + i + ")";
1181 }
1182 return getUtf8(list.get(i));
1183 }
1184 }
1185
1186 final String def = getKernelQedeqBo().getOriginalLanguage();
1187 for (int i = 0; i < list.size(); i++) {
1188 if (EqualsUtility.equals(def, list.get(i).getLanguage())) {
1189 if (method.length() > 0) {
1190 subContext = method + ".get(" + i + ")";
1191 }
1192 return "MISSING! OTHER: " + getUtf8(list.get(i));
1193 }
1194 }
1195
1196 for (int i = 0; i < list.size(); i++) {
1197 if (method.length() > 0) {
1198 subContext = method + ".get(" + i + ")";
1199 }
1200 if (null != list.get(i) && null != list.get(i).getLatex()
1201 && list.get(i).getLatex().trim().length() > 0) {
1202 return "MISSING! OTHER: " + getUtf8(list.get(i));
1203 }
1204 }
1205 return "MISSING!";
1206 } finally {
1207 if (method.length() > 0) {
1208 subContext = "";
1209 }
1210 }
1211 }
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222 private ModuleContext getCurrentContext(final SourcePosition startDelta,
1223 final SourcePosition endDelta) {
1224 if (subContext.length() == 0) {
1225 return super.getCurrentContext();
1226 }
1227 final ModuleContext c = new ModuleContext(super.getCurrentContext().getModuleLocation(),
1228 super.getCurrentContext().getLocationWithinModule() + "." + subContext,
1229 startDelta, endDelta);
1230 return c;
1231 }
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243 public void addWarning(final int code, final String msg, final SourcePosition startDelta,
1244 final SourcePosition endDelta) {
1245 Trace.param(CLASS, this, "addWarning", "msg", msg);
1246 if (addWarnings) {
1247 addWarning(new UnicodeException(code, msg, getCurrentContext(startDelta,
1248 endDelta)));
1249 }
1250 }
1251
1252
1253
1254
1255
1256
1257
1258 public void addWarning(final int code, final String msg) {
1259 Trace.param(CLASS, this, "addWarning", "msg", msg);
1260 if (addWarnings) {
1261 addWarning(new UnicodeException(code, msg, getCurrentContext()));
1262 }
1263 }
1264
1265
1266
1267
1268
1269
1270
1271
1272 protected String[] getUtf8(final Element element, final int max) {
1273 return getKernelQedeqBo().getElement2Utf8().getUtf8(element, max);
1274 }
1275
1276
1277
1278
1279
1280
1281
1282
1283 protected String getUtf8(final Element element) {
1284 return getUtf8(getKernelQedeqBo().getElement2Latex().getLatex(element));
1285 }
1286
1287
1288
1289
1290
1291
1292
1293 private String getUtf8(final Latex latex) {
1294 if (latex == null || latex.getLatex() == null) {
1295 return "";
1296 }
1297 return getUtf8(latex.getLatex());
1298 }
1299
1300
1301
1302
1303
1304
1305
1306 private String getUtf8(final String latex) {
1307 if (latex == null) {
1308 return "";
1309 }
1310 return Latex2UnicodeParser.transform(this, latex, maxColumns);
1311 }
1312
1313
1314
1315
1316
1317
1318 private void underlineBig(final String text) {
1319 printer.println(text);
1320 for (int i = 0; i < text.length(); i++) {
1321 printer.print("\u2550");
1322 }
1323 printer.println();
1324 }
1325
1326
1327
1328
1329
1330
1331 private void underline(final String text) {
1332 printer.println(text);
1333 for (int i = 0; i < text.length(); i++) {
1334 printer.print("\u2015");
1335 }
1336 printer.println();
1337 }
1338
1339 public String getReferenceLink(final String reference, final SourcePosition start,
1340 final SourcePosition end) {
1341 final Reference ref = getReference(reference, getCurrentContext(start, end), addWarnings,
1342 false);
1343
1344 if (ref.isNodeLocalReference() && ref.isSubReference()) {
1345 return "(" + ref.getSubLabel() + ")";
1346 }
1347
1348 if (ref.isNodeLocalReference() && ref.isProofLineReference()) {
1349 return "(" + ref.getProofLineLabel() + ")";
1350 }
1351
1352 if (!ref.isExternal()) {
1353 return getNodeDisplay(ref.getNodeLabel(), ref.getNode())
1354 + (ref.isSubReference() ? " (" + ref.getSubLabel() + ")" : "")
1355 + (ref.isProofLineReference() ? " (" + ref.getProofLineLabel() + ")" : "");
1356 }
1357
1358
1359 if (ref.isExternalModuleReference()) {
1360 return "[" + ref.getExternalQedeqLabel() + "]";
1361 }
1362
1363 return getNodeDisplay(ref.getNodeLabel(), ref.getNode())
1364 + (ref.isSubReference() ? " (" + ref.getSubLabel() + ")" : "")
1365 + (ref.isProofLineReference() ? " (" + ref.getProofLineLabel() + ")" : "")
1366 + (ref.isExternal() ? " [" + ref.getExternalQedeqLabel() + "]" : "");
1367 }
1368
1369 private String getNodeDisplay(final String label, final KernelNodeBo kNode) {
1370 return getNodeDisplay(label, kNode, language);
1371 }
1372
1373 }