0001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
0002 *
0003 * Copyright 2000-2011, Michael Meyling <mime@qedeq.org>.
0004 *
0005 * "Hilbert II" is free software; you can redistribute
0006 * it and/or modify it under the terms of the GNU General Public
0007 * License as published by the Free Software Foundation; either
0008 * version 2 of the License, or (at your option) any later version.
0009 *
0010 * This program is distributed in the hope that it will be useful,
0011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
0012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
0013 * GNU General Public License for more details.
0014 */
0015
0016 package org.qedeq.kernel.bo.service.unicode;
0017
0018 import java.io.IOException;
0019 import java.util.ArrayList;
0020 import java.util.List;
0021
0022 import org.qedeq.base.io.AbstractOutput;
0023 import org.qedeq.base.io.SourcePosition;
0024 import org.qedeq.base.io.TextOutput;
0025 import org.qedeq.base.trace.Trace;
0026 import org.qedeq.base.utility.DateUtility;
0027 import org.qedeq.base.utility.StringUtility;
0028 import org.qedeq.kernel.bo.module.ControlVisitor;
0029 import org.qedeq.kernel.bo.module.KernelNodeBo;
0030 import org.qedeq.kernel.bo.module.KernelQedeqBo;
0031 import org.qedeq.kernel.bo.module.Reference;
0032 import org.qedeq.kernel.se.base.list.Element;
0033 import org.qedeq.kernel.se.base.list.ElementList;
0034 import org.qedeq.kernel.se.base.module.Add;
0035 import org.qedeq.kernel.se.base.module.Author;
0036 import org.qedeq.kernel.se.base.module.AuthorList;
0037 import org.qedeq.kernel.se.base.module.Axiom;
0038 import org.qedeq.kernel.se.base.module.Chapter;
0039 import org.qedeq.kernel.se.base.module.Existential;
0040 import org.qedeq.kernel.se.base.module.FormalProof;
0041 import org.qedeq.kernel.se.base.module.FormalProofLine;
0042 import org.qedeq.kernel.se.base.module.FunctionDefinition;
0043 import org.qedeq.kernel.se.base.module.Header;
0044 import org.qedeq.kernel.se.base.module.Import;
0045 import org.qedeq.kernel.se.base.module.ImportList;
0046 import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
0047 import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
0048 import org.qedeq.kernel.se.base.module.Latex;
0049 import org.qedeq.kernel.se.base.module.LatexList;
0050 import org.qedeq.kernel.se.base.module.LinkList;
0051 import org.qedeq.kernel.se.base.module.LiteratureItem;
0052 import org.qedeq.kernel.se.base.module.LiteratureItemList;
0053 import org.qedeq.kernel.se.base.module.LocationList;
0054 import org.qedeq.kernel.se.base.module.ModusPonens;
0055 import org.qedeq.kernel.se.base.module.Node;
0056 import org.qedeq.kernel.se.base.module.PredicateDefinition;
0057 import org.qedeq.kernel.se.base.module.Proof;
0058 import org.qedeq.kernel.se.base.module.Proposition;
0059 import org.qedeq.kernel.se.base.module.Qedeq;
0060 import org.qedeq.kernel.se.base.module.Rename;
0061 import org.qedeq.kernel.se.base.module.Rule;
0062 import org.qedeq.kernel.se.base.module.Section;
0063 import org.qedeq.kernel.se.base.module.Specification;
0064 import org.qedeq.kernel.se.base.module.Subsection;
0065 import org.qedeq.kernel.se.base.module.SubstFree;
0066 import org.qedeq.kernel.se.base.module.SubstFunc;
0067 import org.qedeq.kernel.se.base.module.SubstPred;
0068 import org.qedeq.kernel.se.base.module.Universal;
0069 import org.qedeq.kernel.se.base.module.UsedByList;
0070 import org.qedeq.kernel.se.common.ModuleAddress;
0071 import org.qedeq.kernel.se.common.ModuleContext;
0072 import org.qedeq.kernel.se.common.ModuleDataException;
0073 import org.qedeq.kernel.se.common.Plugin;
0074 import org.qedeq.kernel.se.common.SourceFileExceptionList;
0075 import org.qedeq.kernel.se.visitor.QedeqNumbers;
0076
0077
0078 /**
0079 * Transfer a QEDEQ module into unicode text.
0080 * <p>
0081 * <b>This is just a quick written generator. This class just generates some text output to be able
0082 * to get a visual impression of a QEDEQ module.</b>
0083 *
0084 * @author Michael Meyling
0085 */
0086 public class Qedeq2UnicodeVisitor extends ControlVisitor implements ReferenceFinder {
0087
0088 /** This class. */
0089 private static final Class CLASS = Qedeq2UnicodeVisitor.class;
0090
0091 /** Output goes here. */
0092 private AbstractOutput printer;
0093
0094 /** Filter text to get and produce text in this language. */
0095 private String language;
0096
0097 /** Filter for this detail level. */
0098 // private String level;
0099
0100 /** Should additional information be put into LaTeX output? E.g. QEDEQ reference names. */
0101 private final boolean info;
0102
0103 /** Current node id. */
0104 private String id;
0105
0106 /** Current node title. */
0107 private String title;
0108
0109 /** Sub context like "getIntroduction()". */
0110 private String subContext = "";
0111
0112 /** Maximum column number. If zero no line breaking is done automatically. */
0113 private int maxColumns;
0114
0115 /** Should warning messages be generated if LaTeX problems occur? */
0116 private boolean addWarnings;
0117
0118 /** Alphabet for tagging. */
0119 private static final String ALPHABET = "abcdefghijklmnopqrstuvwxyz";
0120
0121 /** String representation of formal proof line formula. */
0122 private String[] formula = new String[0];
0123
0124 /** String representation of formal proof line reason. */
0125 private String[] reason = new String[0];
0126
0127 /** This is the maximal formula width. All proof line formulas that are bigger are wrapped. */
0128 private int formulaWidth = 60;
0129
0130 /** This is the maximal reason width. All proof line reasons that are bigger are wrapped. */
0131 private int reasonWidth = 35;
0132
0133 /**
0134 * Constructor.
0135 *
0136 * @param plugin This plugin we work for.
0137 * @param prop QEDEQ BO object.
0138 * @param info Write reference info?
0139 * @param maximumColumn Maximum column before automatic break.
0140 * 0 means no automatic break.
0141 * @param addWarnings Should warning messages be generated
0142 * if LaTeX problems occur?
0143 */
0144 public Qedeq2UnicodeVisitor(final Plugin plugin, final KernelQedeqBo prop,
0145 final boolean info, final int maximumColumn, final boolean addWarnings) {
0146 super(plugin, prop);
0147 this.info = info;
0148 this.maxColumns = maximumColumn;
0149 this.addWarnings = addWarnings;
0150 }
0151
0152 /**
0153 * Gives a UTF-8 representation of given QEDEQ module as InputStream.
0154 *
0155 * @param printer Print herein.
0156 * @param language Filter text to get and produce text in this language only.
0157 * @param level Filter for this detail level. LATER 20100205 m31: not yet supported
0158 * yet.
0159 * @throws SourceFileExceptionList Major problem occurred.
0160 * @throws IOException File IO failed.
0161 */
0162 public void generateUtf8(final AbstractOutput printer, final String language,
0163 final String level) throws SourceFileExceptionList, IOException {
0164 this.printer = printer;
0165 this.printer.setColumns(maxColumns);
0166 // TODO 20110208 m31: perhaps we should have some config parameters for those percentage splittings
0167 if (maxColumns <= 0) {
0168 formulaWidth = 80;
0169 reasonWidth = 50;
0170 } else if (maxColumns <= 50) {
0171 this.printer.setColumns(50);
0172 formulaWidth = 21;
0173 reasonWidth = 21;
0174 } else if (maxColumns <= 100) {
0175 formulaWidth = (maxColumns - 8) * 50 / 100;
0176 reasonWidth = (maxColumns - 8) * 50 / 100;
0177 } else if (maxColumns <= 120) {
0178 reasonWidth = 46 + (maxColumns - 100) / 5;
0179 formulaWidth = maxColumns - 8 - reasonWidth;
0180 } else {
0181 reasonWidth = 50 + (maxColumns - 120) / 10;
0182 formulaWidth = maxColumns - 8 - reasonWidth;
0183 }
0184 // System.out.println("maxColums =" + this.printer.getColumns());
0185 // System.out.println("formulaWidth =" + this.formulaWidth);
0186 // System.out.println("reasonWidth =" + this.reasonWidth);
0187 if (language == null) {
0188 this.language = "en";
0189 } else {
0190 this.language = language;
0191 }
0192 // if (level == null) {
0193 // this.level = "1";
0194 // } else {
0195 // this.level = level;
0196 // }
0197
0198 init();
0199
0200 try {
0201 traverse();
0202 } finally {
0203 getQedeqBo().addPluginErrorsAndWarnings(getPlugin(), getErrorList(), getWarningList());
0204 }
0205 }
0206
0207 /**
0208 * Reset counters and other variables. Should be executed before {@link #traverse()}.
0209 */
0210 protected void init() {
0211 id = null;
0212 title = null;
0213 subContext = "";
0214 }
0215
0216 public final void visitEnter(final Qedeq qedeq) {
0217 if (printer instanceof TextOutput) {
0218 printer.println("================================================================================");
0219 printer.println("UTF-8-file " + ((TextOutput) printer).getName());
0220 printer.println("Generated from " + getQedeqBo().getModuleAddress());
0221 printer.println("Generated at " + DateUtility.getTimestamp());
0222 printer.println("================================================================================");
0223 printer.println();
0224 printer.println("If the characters of this document don't display correctly try opening this");
0225 printer.println("document within a webbrowser and if necessary change the encoding to");
0226 printer.println("Unicode (UTF-8)");
0227 printer.println();
0228 printer.println("Permission is granted to copy, distribute and/or modify this document");
0229 printer.println("under the terms of the GNU Free Documentation License, Version 1.2");
0230 printer.println("or any later version published by the Free Software Foundation;");
0231 printer.println("with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts.");
0232 printer.println();
0233 printer.println();
0234 printer.println();
0235 }
0236 }
0237
0238 public final void visitLeave(final Qedeq qedeq) {
0239 printer.println();
0240 }
0241
0242 public void visitEnter(final Header header) {
0243 final LatexList tit = header.getTitle();
0244 underlineBig(getLatexListEntry("getTitle()", tit));
0245 printer.println();
0246 final AuthorList authors = getQedeqBo().getQedeq().getHeader().getAuthorList();
0247 final StringBuffer authorList = new StringBuffer();
0248 for (int i = 0; i < authors.size(); i++) {
0249 if (i > 0) {
0250 authorList.append(" \n");
0251 printer.println(", ");
0252 }
0253 final Author author = authors.get(i);
0254 final String name = author.getName().getLatex().trim();
0255 printer.print(name);
0256 authorList.append(" " + name);
0257 String email = author.getEmail();
0258 if (email != null && email.trim().length() > 0) {
0259 authorList.append(" <" + email + ">");
0260 }
0261 }
0262 printer.println();
0263 printer.println();
0264 final String url = getQedeqBo().getUrl();
0265 if (url != null && url.length() > 0) {
0266 printer.println();
0267 if ("de".equals(language)) {
0268 printer.println("Die Quelle f\u00FCr dieses Dokument ist hier zu finden:");
0269 } else {
0270 if (!"en".equals(language)) {
0271 printer.println("%%% TODO unknown language: " + language);
0272 }
0273 printer.println("The source for this document can be found here:");
0274 }
0275 printer.println();
0276 printer.println(url);
0277 printer.println();
0278 }
0279 {
0280 printer.println();
0281 if ("de".equals(language)) {
0282 printer.println("Die vorliegende Publikation ist urheberrechtlich gesch\u00FCtzt.");
0283 } else {
0284 if (!"en".equals(language)) {
0285 printer.println("%%% TODO unknown language: " + language);
0286 }
0287 printer.println("Copyright by the authors. All rights reserved.");
0288 }
0289 }
0290 final String email = header.getEmail();
0291 if (email != null && email.length() > 0) {
0292 printer.println();
0293 printer.println();
0294 if ("de".equals(language)) {
0295 printer.println("Bei Fragen, Anregungen oder Bitte um Aufnahme in die Liste der"
0296 + " abh\u00E4ngigen Module schicken Sie bitte eine EMail an die Adresse "
0297 + email);
0298 printer.println();
0299 printer.println();
0300 printer.println("Die Autoren dieses Dokuments sind:");
0301 printer.println();
0302 printer.println(authorList);
0303 } else {
0304 if (!"en".equals(language)) {
0305 printer.println("%%% TODO unknown language: " + language);
0306 }
0307 printer.println("If you have any questions, suggestions or want to add something"
0308 + " to the list of modules that use this one, please send an email to the"
0309 + " address " + email);
0310 printer.println();
0311 printer.println();
0312 printer.println("The authors of this document are:");
0313 printer.println(authorList);
0314 }
0315 printer.println();
0316 }
0317 printer.println();
0318 printer.println();
0319 }
0320
0321 /**
0322 * Get URL for QEDEQ XML module.
0323 *
0324 * @param address Current module address.
0325 * @param specification Find URL for this location list.
0326 * @return URL or <code>""</code> if none (valid?) was found.
0327 */
0328 private String getUrl(final ModuleAddress address, final Specification specification) {
0329 final LocationList list = specification.getLocationList();
0330 if (list == null || list.size() <= 0) {
0331 return "";
0332 }
0333 try {
0334 return address.getModulePaths(specification)[0].getUrl();
0335 } catch (IOException e) {
0336 return "";
0337 }
0338 }
0339
0340 public void visitEnter(final Chapter chapter) {
0341 final QedeqNumbers numbers = getCurrentNumbers();
0342 if (numbers.isChapterNumbering()) {
0343 if ("de".equals(language)) {
0344 printer.println("Kapitel " + numbers.getChapterNumber() + " ");
0345 } else {
0346 printer.println("Chapter " + numbers.getChapterNumber() + " ");
0347 }
0348 printer.println();
0349 printer.println();
0350 }
0351 underlineBig(getLatexListEntry("getTitle()", chapter.getTitle()));
0352 printer.println();
0353 if (chapter.getIntroduction() != null) {
0354 printer.append(getLatexListEntry("getIntroduction()", chapter.getIntroduction()));
0355 printer.println();
0356 printer.println();
0357 printer.println();
0358 }
0359 }
0360
0361 public void visitLeave(final Header header) {
0362 printer.println();
0363 printer.println("___________________________________________________");
0364 printer.println();
0365 printer.println();
0366 }
0367
0368 public void visitLeave(final Chapter chapter) {
0369 printer.println();
0370 printer.println("___________________________________________________");
0371 printer.println();
0372 printer.println();
0373 }
0374
0375 public void visitEnter(final Section section) {
0376 final QedeqNumbers numbers = getCurrentNumbers();
0377 final StringBuffer buffer = new StringBuffer();
0378 if (numbers.isChapterNumbering()) {
0379 buffer.append(numbers.getChapterNumber());
0380 }
0381 if (numbers.isSectionNumbering()) {
0382 if (buffer.length() > 0) {
0383 buffer.append(".");
0384 }
0385 buffer.append(numbers.getSectionNumber());
0386 }
0387 if (buffer.length() > 0 && section.getTitle() != null) {
0388 buffer.append(" ");
0389 }
0390 buffer.append(getLatexListEntry("getTitle()", section.getTitle()));
0391 underline(buffer.toString());
0392 printer.println();
0393 if (section.getIntroduction() != null) {
0394 printer.append(getLatexListEntry("getIntroduction()", section.getIntroduction()));
0395 printer.println();
0396 printer.println();
0397 printer.println();
0398 }
0399 }
0400
0401 public void visitLeave(final Section section) {
0402 printer.println();
0403 }
0404
0405 public void visitEnter(final Subsection subsection) {
0406 final QedeqNumbers numbers = getCurrentNumbers();
0407 final StringBuffer buffer = new StringBuffer();
0408 if (numbers.isChapterNumbering()) {
0409 buffer.append(numbers.getChapterNumber());
0410 }
0411 if (numbers.isSectionNumbering()) {
0412 if (buffer.length() > 0) {
0413 buffer.append(".");
0414 }
0415 buffer.append(numbers.getSectionNumber());
0416 }
0417 if (buffer.length() > 0) {
0418 buffer.append(".");
0419 }
0420 buffer.append(numbers.getSubsectionNumber());
0421 if (buffer.length() > 0 && subsection.getTitle() != null) {
0422 buffer.append(" ");
0423 }
0424 if (subsection.getTitle() != null) {
0425 printer.print(buffer.toString());
0426 printer.print(getLatexListEntry("getTitle()", subsection.getTitle()));
0427 }
0428 if (subsection.getId() != null && info) {
0429 printer.print(" [" + subsection.getId() + "]");
0430 }
0431 if (subsection.getTitle() != null) {
0432 printer.println();
0433 printer.println();
0434 }
0435 printer.append(getLatexListEntry("getLatex()", subsection.getLatex()));
0436 printer.println();
0437 printer.println();
0438 }
0439
0440 public void visitEnter(final Node node) {
0441 if (node.getPrecedingText() != null) {
0442 printer.append(getLatexListEntry("getPrecedingText()", node.getPrecedingText()));
0443 printer.println();
0444 printer.println();
0445 }
0446 id = node.getId();
0447 title = null;
0448 if (node.getTitle() != null) {
0449 title = getLatexListEntry("getTitle()", node.getTitle());
0450 }
0451 }
0452
0453 public void visitLeave(final Node node) {
0454 if (node.getSucceedingText() != null) {
0455 printer.append(getLatexListEntry("getSucceedingText()", node.getSucceedingText()));
0456 printer.println();
0457 printer.println();
0458 }
0459 printer.println();
0460 }
0461
0462 public void visitEnter(final Axiom axiom) {
0463 final QedeqNumbers numbers = getCurrentNumbers();
0464 printer.print("\u2609 ");
0465 printer.print("Axiom " + numbers.getAxiomNumber());
0466 printer.print(" ");
0467 if (title != null && title.length() > 0) {
0468 printer.print(" (" + title + ")");
0469 }
0470 if (info) {
0471 printer.print(" [" + id + "]");
0472 }
0473 printer.println();
0474 printer.println();
0475 printer.print(" ");
0476 printFormula(axiom.getFormula().getElement());
0477 printer.println();
0478 if (axiom.getDescription() != null) {
0479 printer.append(getLatexListEntry("getDescription()", axiom.getDescription()));
0480 printer.println();
0481 printer.println();
0482 }
0483 }
0484
0485 public void visitEnter(final Proposition proposition) {
0486 final QedeqNumbers numbers = getCurrentNumbers();
0487 printer.print("\u2609 ");
0488 printer.print("Proposition " + numbers.getPropositionNumber());
0489 printer.print(" ");
0490 if (title != null && title.length() > 0) {
0491 printer.print(" (" + title + ")");
0492 }
0493 if (info) {
0494 printer.print(" [" + id + "]");
0495 }
0496 printer.println();
0497 printer.println();
0498 printTopFormula(proposition.getFormula().getElement(), id);
0499 printer.println();
0500 if (proposition.getDescription() != null) {
0501 printer.append(getLatexListEntry("getDescription()", proposition.getDescription()));
0502 printer.println();
0503 printer.println();
0504 }
0505 }
0506
0507 public void visitEnter(final Proof proof) {
0508 if ("de".equals(language)) {
0509 printer.println("Beweis:");
0510 } else {
0511 printer.println("Proof:");
0512 }
0513 printer.append(getLatexListEntry("getNonFormalProof()", proof.getNonFormalProof()));
0514 printer.println();
0515 printer.println("q.e.d.");
0516 printer.println();
0517 }
0518
0519 public void visitEnter(final FormalProof proof) {
0520 if ("de".equals(language)) {
0521 printer.println("Beweis (formal):");
0522 } else {
0523 printer.println("Proof (formal):");
0524 }
0525 }
0526
0527 public void visitEnter(final FormalProofLine line) {
0528 if (line.getLabel() != null) {
0529 printer.print(StringUtility.alignRight("(" + line.getLabel() + ")", 5) + " ");
0530 }
0531 if (line.getReasonType() != null && line.getReasonType().getReason() != null) {
0532 setReason(line.getReasonType().getReason().toString());
0533 } else {
0534 reason = new String[0];
0535 }
0536 if (line.getFormula() != null) {
0537 formula = getQedeqBo().getElement2Utf8().getUtf8(line.getFormula().getElement(), formulaWidth);
0538 } else {
0539 formula = new String[0];
0540 }
0541 }
0542
0543 public void visitLeave(final FormalProofLine line) {
0544 int to = Math.max(formula.length, reason.length);
0545 for (int i = 0; i < to; i++) {
0546 printer.skipToColumn(6);
0547 if (i < formula.length) {
0548 printer.print(formula[i]);
0549 }
0550 if (i < reason.length) {
0551 printer.skipToColumn(6 + 2 + formulaWidth);
0552 printer.print(reason[i]);
0553 }
0554 printer.println();
0555 }
0556 }
0557
0558 private void setReason(final String reasonString) {
0559 final List list = new ArrayList();
0560 int index = 0;
0561 while (index < reasonString.length()) {
0562 list.add(StringUtility.substring(reasonString, index, reasonWidth));
0563 index += reasonWidth;
0564 }
0565 reason = (String[]) list.toArray(new String[] {});
0566 }
0567
0568 private String getReference(final String reference) {
0569 return getReference(reference, "getReference()");
0570 }
0571
0572 private String getReference(final String reference, final String subContext) {
0573 final String context = getCurrentContext().getLocationWithinModule();
0574 try {
0575 getCurrentContext().setLocationWithinModule(context + "." + subContext);
0576 return (getReferenceLink(reference, null, null));
0577 } finally {
0578 getCurrentContext().setLocationWithinModule(context);
0579 }
0580 }
0581
0582 public void visitEnter(final ModusPonens r) throws ModuleDataException {
0583 String buffer = r.getName();
0584 boolean one = false;
0585 if (r.getReference1() != null) {
0586 buffer += " " + getReference(r.getReference1(), "getReference1()");
0587 one = true;
0588 }
0589 if (r.getReference1() != null) {
0590 if (one) {
0591 buffer += ",";
0592 }
0593 buffer += " " + getReference(r.getReference2(), "getReference2()");
0594 }
0595 setReason(buffer);
0596 }
0597
0598 public void visitEnter(final Add r) throws ModuleDataException {
0599 String buffer = r.getName();
0600 if (r.getReference() != null) {
0601 buffer += " " + getReference(r.getReference());
0602 }
0603 setReason(buffer);
0604 }
0605
0606 public void visitEnter(final Rename r) throws ModuleDataException {
0607 String buffer = r.getName();
0608 if (r.getOriginalSubjectVariable() != null) {
0609 buffer += " " + getQedeqBo().getElement2Utf8().getUtf8(
0610 r.getOriginalSubjectVariable());
0611 }
0612 if (r.getReplacementSubjectVariable() != null) {
0613 buffer += " by " + getQedeqBo().getElement2Utf8().getUtf8(
0614 r.getReplacementSubjectVariable());
0615 }
0616 if (r.getReference() != null) {
0617 buffer += " in " + getReference(r.getReference());
0618 }
0619 setReason(buffer);
0620 }
0621
0622 public void visitEnter(final SubstFree r) throws ModuleDataException {
0623 String buffer = r.getName();
0624 if (r.getSubjectVariable() != null) {
0625 buffer += " " + getQedeqBo().getElement2Utf8().getUtf8(
0626 r.getSubjectVariable());
0627 }
0628 if (r.getSubstituteTerm() != null) {
0629 buffer += " by " + getQedeqBo().getElement2Utf8().getUtf8(
0630 r.getSubstituteTerm());
0631 }
0632 if (r.getReference() != null) {
0633 buffer += " in " + getReference(r.getReference());
0634 }
0635 setReason(buffer);
0636 }
0637
0638 public void visitEnter(final SubstFunc r) throws ModuleDataException {
0639 String buffer = r.getName();
0640 if (r.getFunctionVariable() != null) {
0641 buffer += " " + getQedeqBo().getElement2Utf8().getUtf8(
0642 r.getFunctionVariable());
0643 }
0644 if (r.getSubstituteTerm() != null) {
0645 buffer += " by " + getQedeqBo().getElement2Utf8().getUtf8(
0646 r.getSubstituteTerm());
0647 }
0648 if (r.getReference() != null) {
0649 buffer += " in " + getReference(r.getReference());
0650 }
0651 setReason(buffer);
0652 }
0653
0654 public void visitEnter(final SubstPred r) throws ModuleDataException {
0655 String buffer = r.getName();
0656 if (r.getPredicateVariable() != null) {
0657 buffer += " " + getQedeqBo().getElement2Utf8().getUtf8(
0658 r.getPredicateVariable());
0659 }
0660 if (r.getSubstituteFormula() != null) {
0661 buffer += " by " + getQedeqBo().getElement2Utf8().getUtf8(
0662 r.getSubstituteFormula());
0663 }
0664 if (r.getReference() != null) {
0665 buffer += " in " + getReference(r.getReference());
0666 }
0667 setReason(buffer);
0668 }
0669
0670 public void visitEnter(final Existential r) throws ModuleDataException {
0671 String buffer = r.getName();
0672 if (r.getSubjectVariable() != null) {
0673 buffer += " with " + getQedeqBo().getElement2Utf8().getUtf8(
0674 r.getSubjectVariable());
0675 }
0676 if (r.getReference() != null) {
0677 buffer += " in " + getReference(r.getReference());
0678 }
0679 setReason(buffer);
0680 }
0681
0682 public void visitEnter(final Universal r) throws ModuleDataException {
0683 String buffer = r.getName();
0684 if (r.getSubjectVariable() != null) {
0685 buffer += " with " + getQedeqBo().getElement2Utf8().getUtf8(
0686 r.getSubjectVariable());
0687 }
0688 if (r.getReference() != null) {
0689 buffer += " in " + getReference(r.getReference());
0690 }
0691 setReason(buffer);
0692 }
0693 public void visitLeave(final FormalProof proof) {
0694 printer.println();
0695 printer.println("q.e.d.");
0696 printer.println();
0697 }
0698
0699 public void visitEnter(final InitialPredicateDefinition definition) {
0700 final QedeqNumbers numbers = getCurrentNumbers();
0701 printer.print("\u2609 ");
0702 final StringBuffer buffer = new StringBuffer();
0703 if ("de".equals(language)) {
0704 buffer.append("initiale ");
0705 } else {
0706 buffer.append("initial ");
0707 }
0708 buffer.append("Definition " + (numbers.getPredicateDefinitionNumber()
0709 + numbers.getFunctionDefinitionNumber()));
0710 printer.print(buffer.toString());
0711 printer.print(" ");
0712 if (title != null && title.length() > 0) {
0713 printer.print(" (" + title + ")");
0714 }
0715 if (info) {
0716 printer.print(" [" + id + "]");
0717 }
0718 printer.println();
0719 printer.println();
0720 printer.print(" ");
0721 printer.println(getUtf8(definition.getPredCon()));
0722 printer.println();
0723 if (definition.getDescription() != null) {
0724 printer.append(getLatexListEntry("getDescription()", definition.getDescription()));
0725 printer.println();
0726 printer.println();
0727 }
0728 }
0729
0730 public void visitEnter(final PredicateDefinition definition) {
0731 final QedeqNumbers numbers = getCurrentNumbers();
0732 printer.print("\u2609 ");
0733 final StringBuffer buffer = new StringBuffer();
0734 buffer.append("Definition " + (numbers.getPredicateDefinitionNumber()
0735 + numbers.getFunctionDefinitionNumber()));
0736 printer.print(buffer.toString());
0737 printer.print(" ");
0738 if (title != null && title.length() > 0) {
0739 printer.print(" (" + title + ")");
0740 }
0741 if (info) {
0742 printer.print(" [" + id + "]");
0743 }
0744 printer.println();
0745 printer.println();
0746 printer.print(" ");
0747 printer.println(getUtf8(definition.getFormula().getElement()));
0748 printer.println();
0749 if (definition.getDescription() != null) {
0750 printer.append(getLatexListEntry("getDescription()", definition.getDescription()));
0751 printer.println();
0752 printer.println();
0753 }
0754 }
0755
0756 public void visitEnter(final InitialFunctionDefinition definition) {
0757 final QedeqNumbers numbers = getCurrentNumbers();
0758 printer.print("\u2609 ");
0759 final StringBuffer buffer = new StringBuffer();
0760 if ("de".equals(language)) {
0761 buffer.append("initiale ");
0762 } else {
0763 buffer.append("initial ");
0764 }
0765 buffer.append("Definition " + (numbers.getPredicateDefinitionNumber()
0766 + numbers.getFunctionDefinitionNumber()));
0767 printer.print(buffer.toString());
0768 printer.print(" ");
0769 if (title != null && title.length() > 0) {
0770 printer.print(" (" + title + ")");
0771 }
0772 if (info) {
0773 printer.print(" [" + id + "]");
0774 }
0775 printer.println();
0776 printer.println();
0777 printer.print(" ");
0778 printer.println(getUtf8(definition.getFunCon()));
0779 printer.println();
0780 if (definition.getDescription() != null) {
0781 printer.println(getLatexListEntry("getDescription()", definition.getDescription()));
0782 printer.println();
0783 }
0784 }
0785
0786 public void visitEnter(final FunctionDefinition definition) {
0787 final QedeqNumbers numbers = getCurrentNumbers();
0788 printer.print("\u2609 ");
0789 final StringBuffer buffer = new StringBuffer();
0790 buffer.append("Definition " + (numbers.getPredicateDefinitionNumber()
0791 + numbers.getFunctionDefinitionNumber()));
0792 printer.print(buffer.toString());
0793 printer.print(" ");
0794 if (title != null && title.length() > 0) {
0795 printer.print(" (" + title + ")");
0796 }
0797 if (info) {
0798 printer.print(" [" + id + "]");
0799 }
0800 printer.println();
0801 printer.println();
0802 printer.print(" ");
0803 printer.println(getUtf8(definition.getFormula().getElement()));
0804 printer.println();
0805 if (definition.getDescription() != null) {
0806 printer.println(getLatexListEntry("getDescription()", definition.getDescription()));
0807 printer.println();
0808 }
0809 }
0810
0811 public void visitEnter(final Rule rule) {
0812 final QedeqNumbers numbers = getCurrentNumbers();
0813 printer.print("\u2609 ");
0814 if ("de".equals(language)) {
0815 printer.print("Regel");
0816 } else {
0817 printer.print("Rule");
0818 }
0819 printer.print(" " + numbers.getRuleNumber());
0820 printer.print(" ");
0821 if (title != null && title.length() > 0) {
0822 printer.print(" (" + title + ")");
0823 }
0824 if (info) {
0825 printer.print(" [" + id + "]");
0826 }
0827 printer.println();
0828 printer.println();
0829 if (rule.getDescription() != null) {
0830 printer.append(getLatexListEntry("getDescription()", rule.getDescription()));
0831 printer.println();
0832 printer.println();
0833 }
0834 if (rule.getProofList() != null) {
0835 for (int i = 0; i < rule.getProofList().size(); i++) {
0836 if ("de".equals(language)) {
0837 printer.println("Beweis:");
0838 } else {
0839 printer.println("Proof:");
0840 }
0841 printer.append(getLatexListEntry("getProofList().get(" + i + ")", rule.getProofList().get(i)
0842 .getNonFormalProof()));
0843 printer.println();
0844 printer.println("q.e.d.");
0845 printer.println();
0846 }
0847 }
0848 }
0849
0850 public void visitEnter(final LinkList linkList) {
0851 if (linkList.size() <= 0) {
0852 return;
0853 }
0854 if ("de".equals(language)) {
0855 printer.println("Basierend auf: ");
0856 } else {
0857 if (!"en".equals(language)) {
0858 printer.println("%%% TODO unknown language: " + language);
0859 }
0860 printer.println("Based on: ");
0861 }
0862 for (int i = 0; i < linkList.size(); i++) {
0863 if (linkList.get(i) != null) {
0864 printer.print(" (" + linkList.get(i) + ")");
0865 }
0866 };
0867 printer.println();
0868 }
0869
0870 public void visitEnter(final LiteratureItemList list) {
0871 printer.println();
0872 printer.println();
0873 if ("de".equals(language)) {
0874 underlineBig("Literaturverzeichnis");
0875 } else {
0876 underlineBig("Bibliography");
0877 }
0878 printer.println();
0879 printer.println();
0880 final ImportList imports = getQedeqBo().getQedeq().getHeader().getImportList();
0881 if (imports != null && imports.size() > 0) {
0882 printer.println();
0883 printer.println();
0884 if ("de".equals(language)) {
0885 printer.println("Benutzte andere QEDEQ-Module:");
0886 } else {
0887 printer.println("Used other QEDEQ modules:");
0888 }
0889 printer.println();
0890 for (int i = 0; i < imports.size(); i++) {
0891 final Import imp = imports.get(i);
0892 printer.print("[" + imp.getLabel() + "] ");
0893 final Specification spec = imp.getSpecification();
0894 printer.print(spec.getName());
0895 if (spec.getLocationList() != null && spec.getLocationList().size() > 0
0896 && spec.getLocationList().get(0).getLocation().length() > 0) {
0897 printer.print(" ");
0898 printer.print(getUrl(getQedeqBo().getModuleAddress(), spec));
0899 }
0900 printer.println();
0901 }
0902 printer.println();
0903 printer.println();
0904 if ("de".equals(language)) {
0905 printer.println("Andere Referenzen:");
0906 } else {
0907 printer.println("Other references:");
0908 }
0909 printer.println();
0910 }
0911 }
0912
0913 public void visitLeave(final LiteratureItemList list) {
0914 final UsedByList usedby = getQedeqBo().getQedeq().getHeader().getUsedByList();
0915 if (usedby != null && usedby.size() > 0) {
0916 printer.println();
0917 printer.println();
0918 if ("de".equals(language)) {
0919 printer.println("QEDEQ-Module, welche dieses hier verwenden:");
0920 } else {
0921 printer.println("QEDEQ modules that use this one:");
0922 }
0923 for (int i = 0; i < usedby.size(); i++) {
0924 final Specification spec = usedby.get(i);
0925 printer.print(spec.getName());
0926 final String url = getUrl(getQedeqBo().getModuleAddress(), spec);
0927 if (url != null && url.length() > 0) {
0928 printer.print(" ");
0929 printer.print(url);
0930 }
0931 printer.println();
0932 }
0933 printer.println();
0934 printer.println();
0935 }
0936 printer.println();
0937 }
0938
0939 public void visitEnter(final LiteratureItem item) {
0940 printer.print("[" + item.getLabel() + "] ");
0941 printer.println(getLatexListEntry("getItem()", item.getItem()));
0942 printer.println();
0943 }
0944
0945 /**
0946 * Print top level formula. If the formula has the form <code>AND(.., .., ..)</code> the
0947 * formula is broken down in several labeled lines.
0948 *
0949 * @param element Formula to print.
0950 * @param mainLabel Main formula label.
0951 */
0952 private void printTopFormula(final Element element, final String mainLabel) {
0953 if (!element.isList() || !element.getList().getOperator().equals("AND")) {
0954 printer.print(" ");
0955 printFormula(element);
0956 return;
0957 }
0958 final ElementList list = element.getList();
0959 for (int i = 0; i < list.size(); i++) {
0960 String label = "";
0961 if (list.size() >= ALPHABET.length() * ALPHABET.length()) {
0962 label = "" + (i + 1);
0963 } else {
0964 if (list.size() > ALPHABET.length()) {
0965 final int div = (i / ALPHABET.length());
0966 label = "" + ALPHABET.charAt(div);
0967 }
0968 label += ALPHABET.charAt(i % ALPHABET.length());
0969 }
0970 printer.println(" (" + label + ") " + getUtf8(list.getElement(i)));
0971 }
0972 }
0973
0974 /**
0975 * Print formula.
0976 *
0977 * @param element Formula to print.
0978 */
0979 private void printFormula(final Element element) {
0980 printer.println(getUtf8(element));
0981 }
0982
0983 /**
0984 * Get Utf8 element presentation.
0985 *
0986 * @param element Get presentation of this element.
0987 * @return UTF-8 form of element.
0988 */
0989 private String getUtf8(final Element element) {
0990 return getUtf8(getQedeqBo().getElement2Latex().getLatex(element));
0991 }
0992
0993 /**
0994 * Filters correct entry out of LaTeX list. Filter criterion is for example the correct
0995 * language.
0996 *
0997 * @param method This method was called. Used to get the correct sub context.
0998 * Should not be null. If it is empty the <code>subContext</code>
0999 * is not changed.
1000 * @param list List of LaTeX texts.
1001 * @return Filtered text.
1002 */
1003 private String getLatexListEntry(final String method, final LatexList list) {
1004 if (list == null) {
1005 return "";
1006 }
1007 if (method.length() > 0) {
1008 subContext = method;
1009 }
1010 try {
1011 for (int i = 0; i < list.size(); i++) {
1012 if (language.equals(list.get(i).getLanguage())) {
1013 if (method.length() > 0) {
1014 subContext = method + ".get(" + i + ")";
1015 }
1016 return getUtf8(list.get(i));
1017 }
1018 }
1019 // assume entry with missing language as default
1020 for (int i = 0; i < list.size(); i++) {
1021 if (list.get(i).getLanguage() == null) {
1022 if (method.length() > 0) {
1023 subContext = method + ".get(" + i + ")";
1024 }
1025 return getUtf8(list.get(i));
1026 }
1027 }
1028 for (int i = 0; i < list.size(); i++) { // LATER mime 20050222: evaluate default?
1029 if (method.length() > 0) {
1030 subContext = method + ".get(" + i + ")";
1031 }
1032 return "MISSING! OTHER: " + getUtf8(list.get(i));
1033 }
1034 return "MISSING!";
1035 } finally {
1036 if (method.length() > 0) {
1037 subContext = "";
1038 }
1039 }
1040 }
1041
1042 /**
1043 * Get current module context. Uses sub context information.
1044 *
1045 * @param startDelta Skip position (relative to location start). Could be
1046 * <code>null</code>.
1047 * @param endDelta Mark until this column (relative to location start).
1048 * be <code>null</code>
1049 * @return Current module context.
1050 */
1051 private ModuleContext getCurrentContext(final SourcePosition startDelta,
1052 final SourcePosition endDelta) {
1053 if (subContext.length() == 0) {
1054 return super.getCurrentContext();
1055 }
1056 final ModuleContext c = new ModuleContext(super.getCurrentContext().getModuleLocation(),
1057 super.getCurrentContext().getLocationWithinModule() + "." + subContext,
1058 startDelta, endDelta);
1059 return c;
1060 }
1061
1062 /**
1063 * Add warning.
1064 *
1065 * @param code Warning code.
1066 * @param msg Warning message.
1067 * @param startDelta Skip position (relative to location start). Could be
1068 * <code>null</code>.
1069 * @param endDelta Mark until this column (relative to location start). Could be
1070 * be <code>null</code>
1071 */
1072 public void addWarning(final int code, final String msg, final SourcePosition startDelta,
1073 final SourcePosition endDelta) {
1074 Trace.param(CLASS, this, "addWarning", "msg", msg);
1075 if (addWarnings) {
1076 addWarning(new UnicodeException(code, msg, getCurrentContext(startDelta,
1077 endDelta)));
1078 }
1079 }
1080
1081 /**
1082 * Add warning.
1083 *
1084 * @param code Warning code.
1085 * @param msg Warning message.
1086 */
1087 public void addWarning(final int code, final String msg) {
1088 Trace.param(CLASS, this, "addWarning", "msg", msg);
1089 if (addWarnings) {
1090 addWarning(new UnicodeException(code, msg, getCurrentContext()));
1091 }
1092 }
1093
1094 /**
1095 * Get UTF-8 String for LaTeX.
1096 *
1097 * @param latex LaTeX we got.
1098 * @return UTF-8 result string.
1099 */
1100 private String getUtf8(final Latex latex) {
1101 if (latex == null || latex.getLatex() == null) {
1102 return "";
1103 }
1104 return getUtf8(latex.getLatex());
1105 }
1106
1107 /**
1108 * Transform LaTeX into UTF-8 String..
1109 *
1110 * @param latex LaTeX text.
1111 * @return String.
1112 */
1113 private String getUtf8(final String latex) {
1114 if (latex == null) {
1115 return "";
1116 }
1117 return Latex2UnicodeParser.transform(this, latex, maxColumns);
1118 }
1119
1120 /**
1121 * Print text in one line and print another line with = to underline it.
1122 *
1123 * @param text Line to print.
1124 */
1125 private void underlineBig(final String text) {
1126 printer.println(text);
1127 for (int i = 0; i < text.length(); i++) {
1128 printer.print("\u2550");
1129 }
1130 printer.println();
1131 }
1132
1133 /**
1134 * Print text in one line and print another line with = to underline it.
1135 *
1136 * @param text Line to print.
1137 */
1138 private void underline(final String text) {
1139 printer.println(text);
1140 for (int i = 0; i < text.length(); i++) {
1141 printer.print("\u2015");
1142 }
1143 printer.println();
1144 }
1145
1146 public String getReferenceLink(final String reference, final SourcePosition start,
1147 final SourcePosition end) {
1148 final Reference ref = getReference(reference, getCurrentContext(start, end), addWarnings,
1149 false);
1150
1151 if (ref.isNodeLocalReference() && ref.isSubReference()) {
1152 return "(" + ref.getSubLabel() + ")";
1153 }
1154
1155 if (ref.isNodeLocalReference() && ref.isProofLineReference()) {
1156 return "(" + ref.getProofLineLabel() + ")";
1157 }
1158
1159 if (!ref.isExternal()) {
1160 return getNodeDisplay(ref.getNodeLabel(), ref.getNode())
1161 + (ref.isSubReference() ? " (" + ref.getSubLabel() + ")" : "")
1162 + (ref.isProofLineReference() ? " (" + ref.getProofLineLabel() + ")" : "");
1163 }
1164
1165 // do we have an external module reference without node?
1166 if (ref.isExternalModuleReference()) {
1167 return "[" + ref.getExternalQedeqLabel() + "]";
1168 }
1169
1170 return getNodeDisplay(ref.getNodeLabel(), ref.getNode())
1171 + (ref.isSubReference() ? " (" + ref.getSubLabel() + ")" : "")
1172 + (ref.isProofLineReference() ? " (" + ref.getProofLineLabel() + ")" : "")
1173 + (ref.isExternal() ? " [" + ref.getExternalQedeqLabel() + "]" : "");
1174 }
1175
1176 private String getNodeDisplay(final String label, final KernelNodeBo kNode) {
1177 return getNodeDisplay(label, kNode, language);
1178 }
1179
1180 }
|