0001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
0002 *
0003 * Copyright 2000-2013, 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.se.visitor;
0017
0018 import java.util.HashMap;
0019 import java.util.Map;
0020 import java.util.Stack;
0021
0022 import org.qedeq.kernel.se.base.list.Atom;
0023 import org.qedeq.kernel.se.base.list.Element;
0024 import org.qedeq.kernel.se.base.list.ElementList;
0025 import org.qedeq.kernel.se.base.module.Add;
0026 import org.qedeq.kernel.se.base.module.Author;
0027 import org.qedeq.kernel.se.base.module.AuthorList;
0028 import org.qedeq.kernel.se.base.module.Axiom;
0029 import org.qedeq.kernel.se.base.module.ChangedRule;
0030 import org.qedeq.kernel.se.base.module.ChangedRuleList;
0031 import org.qedeq.kernel.se.base.module.Chapter;
0032 import org.qedeq.kernel.se.base.module.ChapterList;
0033 import org.qedeq.kernel.se.base.module.Conclusion;
0034 import org.qedeq.kernel.se.base.module.ConditionalProof;
0035 import org.qedeq.kernel.se.base.module.Existential;
0036 import org.qedeq.kernel.se.base.module.FormalProof;
0037 import org.qedeq.kernel.se.base.module.FormalProofLine;
0038 import org.qedeq.kernel.se.base.module.FormalProofLineList;
0039 import org.qedeq.kernel.se.base.module.FormalProofList;
0040 import org.qedeq.kernel.se.base.module.Formula;
0041 import org.qedeq.kernel.se.base.module.FunctionDefinition;
0042 import org.qedeq.kernel.se.base.module.Header;
0043 import org.qedeq.kernel.se.base.module.Hypothesis;
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.Location;
0054 import org.qedeq.kernel.se.base.module.LocationList;
0055 import org.qedeq.kernel.se.base.module.ModusPonens;
0056 import org.qedeq.kernel.se.base.module.Node;
0057 import org.qedeq.kernel.se.base.module.PredicateDefinition;
0058 import org.qedeq.kernel.se.base.module.Proof;
0059 import org.qedeq.kernel.se.base.module.ProofList;
0060 import org.qedeq.kernel.se.base.module.Proposition;
0061 import org.qedeq.kernel.se.base.module.Qedeq;
0062 import org.qedeq.kernel.se.base.module.Reason;
0063 import org.qedeq.kernel.se.base.module.Rename;
0064 import org.qedeq.kernel.se.base.module.Rule;
0065 import org.qedeq.kernel.se.base.module.Section;
0066 import org.qedeq.kernel.se.base.module.SectionList;
0067 import org.qedeq.kernel.se.base.module.Specification;
0068 import org.qedeq.kernel.se.base.module.Subsection;
0069 import org.qedeq.kernel.se.base.module.SubsectionList;
0070 import org.qedeq.kernel.se.base.module.SubstFree;
0071 import org.qedeq.kernel.se.base.module.SubstFunc;
0072 import org.qedeq.kernel.se.base.module.SubstPred;
0073 import org.qedeq.kernel.se.base.module.Term;
0074 import org.qedeq.kernel.se.base.module.Universal;
0075 import org.qedeq.kernel.se.base.module.UsedByList;
0076 import org.qedeq.kernel.se.common.ModuleAddress;
0077 import org.qedeq.kernel.se.common.ModuleContext;
0078 import org.qedeq.kernel.se.common.ModuleDataException;
0079 import org.qedeq.kernel.se.common.RuleKey;
0080 import org.qedeq.kernel.se.dto.module.FormulaVo;
0081 import org.qedeq.kernel.se.dto.module.TermVo;
0082
0083
0084 /**
0085 * Traverse QEDEQ module. Calls visitors of {@link org.qedeq.kernel.se.visitor.QedeqVisitor}
0086 * for non <code>null</code> arguments.
0087 *
0088 * @author Michael Meyling
0089 */
0090 public class QedeqNotNullTraverser implements QedeqTraverser {
0091
0092 /** Current context during creation. */
0093 private final ModuleContext currentContext;
0094
0095 /** Readable traverse location info. */
0096 private final Stack location = new Stack();
0097
0098 /** Herein are various counters for the current node. */
0099 private QedeqNumbers data = new QedeqNumbers(0, 0);
0100
0101 /** Converts chapter and other titles into text. */
0102 private final LatexList2Text transform = new LatexList2Text();
0103
0104 /**
0105 * These methods are called if a node is visited. To start the whole process just call
0106 * {@link #accept(Qedeq)}.
0107 */
0108 private QedeqVisitor visitor;
0109
0110 /** Is sub node traverse currently blocked? */
0111 private boolean blocked;
0112
0113 /** Currently visited node element of QEDEQ module. Might be <code>null</code>. */
0114 private Node node;
0115
0116 /** Maps local {@link ruleName}s to local {@link RuleKey}s. */
0117 private Map ruleExistence;
0118
0119 /**
0120 * Constructor.
0121 *
0122 * @param globalContext Module location information.
0123 * @param visitor These methods are called if a node is visited.
0124 */
0125 public QedeqNotNullTraverser(final ModuleAddress globalContext, final QedeqVisitor visitor) {
0126 currentContext = globalContext.createModuleContext();
0127 this.visitor = visitor;
0128 }
0129
0130 /**
0131 * Constructor.
0132 *
0133 * @param globalContext Module location information.
0134 */
0135 public QedeqNotNullTraverser(final ModuleAddress globalContext) {
0136 currentContext = globalContext.createModuleContext();
0137 }
0138
0139 /**
0140 * Set visitor.
0141 *
0142 * @param visitor These methods are called if a node is visited.
0143 */
0144 public void setVisitor(final QedeqVisitor visitor) {
0145 this.visitor = visitor;
0146 }
0147
0148 public void accept(final Qedeq qedeq) throws ModuleDataException {
0149 ruleExistence = new HashMap();
0150 setLocation("started");
0151 if (qedeq == null) {
0152 throw new NullPointerException("null QEDEQ module");
0153 }
0154 data = new QedeqNumbers(
0155 (qedeq.getHeader() != null && qedeq.getHeader().getImportList() != null
0156 ? qedeq.getHeader().getImportList().size() : 0),
0157 (qedeq.getChapterList() != null ? qedeq.getChapterList().size() : 0)
0158 );
0159 getCurrentContext().setLocationWithinModule("");
0160 checkForInterrupt();
0161 blocked = false;
0162 final String context = getCurrentContext().getLocationWithinModule();
0163 visitor.visitEnter(qedeq);
0164 if (qedeq.getHeader() != null) {
0165 getCurrentContext().setLocationWithinModule(context + "getHeader()");
0166 accept(qedeq.getHeader());
0167 }
0168 if (qedeq.getChapterList() != null) {
0169 getCurrentContext().setLocationWithinModule(context + "getChapterList()");
0170 accept(qedeq.getChapterList());
0171 }
0172 if (qedeq.getLiteratureItemList() != null) {
0173 getCurrentContext().setLocationWithinModule(context + "getLiteratureItemList()");
0174 accept(qedeq.getLiteratureItemList());
0175 }
0176 setLocationWithinModule(context);
0177 visitor.visitLeave(qedeq);
0178 setLocationWithinModule(context);
0179 setLocation("finished");
0180 data.setFinished(true);
0181 }
0182
0183 /**
0184 * Check if current thread is interrupted.
0185 *
0186 * @throws InterruptException We were interrupted.
0187 */
0188 private void checkForInterrupt() throws InterruptException {
0189 if (Thread.interrupted()) {
0190 throw new InterruptException(getCurrentContext());
0191 }
0192 }
0193
0194 public void accept(final Header header) throws ModuleDataException {
0195 checkForInterrupt();
0196 if (blocked || header == null) {
0197 return;
0198 }
0199 setLocation("analyzing header");
0200 final String context = getCurrentContext().getLocationWithinModule();
0201 visitor.visitEnter(header);
0202 if (header.getSpecification() != null) {
0203 setLocationWithinModule(context + ".getSpecification()");
0204 accept(header.getSpecification());
0205 }
0206 if (header.getTitle() != null) {
0207 setLocationWithinModule(context + ".getTitle()");
0208 accept(header.getTitle());
0209 }
0210 if (header.getSummary() != null) {
0211 setLocationWithinModule(context + ".getSummary()");
0212 accept(header.getSummary());
0213 }
0214 if (header.getAuthorList() != null) {
0215 setLocationWithinModule(context + ".getAuthorList()");
0216 accept(header.getAuthorList());
0217 }
0218 if (header.getImportList() != null) {
0219 setLocationWithinModule(context + ".getImportList()");
0220 accept(header.getImportList());
0221 }
0222 if (header.getUsedByList() != null) {
0223 setLocationWithinModule(context + ".getUsedByList()");
0224 accept(header.getUsedByList());
0225 }
0226 setLocationWithinModule(context);
0227 visitor.visitLeave(header);
0228 setLocationWithinModule(context);
0229 }
0230
0231 public void accept(final UsedByList usedByList) throws ModuleDataException {
0232 checkForInterrupt();
0233 if (blocked || usedByList == null) {
0234 return;
0235 }
0236 location.push("working on used by list");
0237 final String context = getCurrentContext().getLocationWithinModule();
0238 visitor.visitEnter(usedByList);
0239 for (int i = 0; i < usedByList.size(); i++) {
0240 setLocationWithinModule(context + ".get(" + i + ")");
0241 accept(usedByList.get(i));
0242 }
0243 setLocationWithinModule(context);
0244 visitor.visitLeave(usedByList);
0245 setLocationWithinModule(context);
0246 location.pop();
0247 }
0248
0249 public void accept(final ImportList importList) throws ModuleDataException {
0250 checkForInterrupt();
0251 if (blocked || importList == null) {
0252 return;
0253 }
0254 location.push("working on import list");
0255 final String context = getCurrentContext().getLocationWithinModule();
0256 visitor.visitEnter(importList);
0257 for (int i = 0; i < importList.size(); i++) {
0258 setLocationWithinModule(context + ".get(" + i + ")");
0259 accept(importList.get(i));
0260 }
0261 setLocationWithinModule(context);
0262 visitor.visitLeave(importList);
0263 setLocationWithinModule(context);
0264 location.pop();
0265 }
0266
0267 public void accept(final Import imp) throws ModuleDataException {
0268 data.increaseImportNumber();
0269 checkForInterrupt();
0270 if (blocked || imp == null) {
0271 return;
0272 }
0273 location.push("import " + data.getImportNumber() + ": " + imp.getLabel());
0274 final String context = getCurrentContext().getLocationWithinModule();
0275 visitor.visitEnter(imp);
0276 if (imp.getSpecification() != null) {
0277 setLocationWithinModule(context + ".getSpecification()");
0278 accept(imp.getSpecification());
0279 }
0280 setLocationWithinModule(context);
0281 visitor.visitLeave(imp);
0282 setLocationWithinModule(context);
0283 location.pop();
0284 }
0285
0286 public void accept(final Specification specification) throws ModuleDataException {
0287 checkForInterrupt();
0288 if (blocked || specification == null) {
0289 return;
0290 }
0291 final String context = getCurrentContext().getLocationWithinModule();
0292 visitor.visitEnter(specification);
0293 if (specification.getLocationList() != null) {
0294 setLocationWithinModule(context + ".getLocationList()");
0295 accept(specification.getLocationList());
0296 }
0297 setLocationWithinModule(context);
0298 visitor.visitLeave(specification);
0299 setLocationWithinModule(context);
0300 }
0301
0302 public void accept(final LocationList locationList) throws ModuleDataException {
0303 checkForInterrupt();
0304 if (blocked || locationList == null) {
0305 return;
0306 }
0307 final String context = getCurrentContext().getLocationWithinModule();
0308 visitor.visitEnter(locationList);
0309 for (int i = 0; i < locationList.size(); i++) {
0310 setLocationWithinModule(context + ".get(" + i + ")");
0311 accept(locationList.get(i));
0312 }
0313 setLocationWithinModule(context);
0314 visitor.visitLeave(locationList);
0315 setLocationWithinModule(context);
0316 }
0317
0318 public void accept(final Location location) throws ModuleDataException {
0319 checkForInterrupt();
0320 if (blocked || location == null) {
0321 return;
0322 }
0323 final String context = getCurrentContext().getLocationWithinModule();
0324 visitor.visitEnter(location);
0325 setLocationWithinModule(context);
0326 visitor.visitLeave(location);
0327 setLocationWithinModule(context);
0328 }
0329
0330 public void accept(final AuthorList authorList) throws ModuleDataException {
0331 checkForInterrupt();
0332 if (blocked || authorList == null) {
0333 return;
0334 }
0335 final String context = getCurrentContext().getLocationWithinModule();
0336 visitor.visitEnter(authorList);
0337 for (int i = 0; i < authorList.size(); i++) {
0338 setLocationWithinModule(context + ".get(" + i + ")");
0339 accept(authorList.get(i));
0340 }
0341 setLocationWithinModule(context);
0342 visitor.visitLeave(authorList);
0343 setLocationWithinModule(context);
0344 }
0345
0346 public void accept(final Author author) throws ModuleDataException {
0347 checkForInterrupt();
0348 if (blocked || author == null) {
0349 return;
0350 }
0351 final String context = getCurrentContext().getLocationWithinModule();
0352 visitor.visitEnter(author);
0353 if (author.getName() != null) {
0354 setLocationWithinModule(context + ".getName()");
0355 accept(author.getName());
0356 }
0357 setLocationWithinModule(context);
0358 visitor.visitLeave(author);
0359 setLocationWithinModule(context);
0360 }
0361
0362 public void accept(final ChapterList chapterList) throws ModuleDataException {
0363 checkForInterrupt();
0364 if (blocked || chapterList == null) {
0365 return;
0366 }
0367 final String context = getCurrentContext().getLocationWithinModule();
0368 visitor.visitEnter(chapterList);
0369 for (int i = 0; i < chapterList.size(); i++) {
0370 setLocationWithinModule(context + ".get(" + i + ")");
0371 accept(chapterList.get(i));
0372 }
0373 setLocationWithinModule(context);
0374 visitor.visitLeave(chapterList);
0375 setLocationWithinModule(context);
0376 }
0377
0378 public void accept(final Chapter chapter) throws ModuleDataException {
0379 checkForInterrupt();
0380 if (blocked || chapter == null) {
0381 return;
0382 }
0383 data.increaseChapterNumber(
0384 (chapter.getSectionList() != null ? chapter.getSectionList().size() : 0),
0385 chapter.getNoNumber() == null || !chapter.getNoNumber().booleanValue()
0386 );
0387 if (data.isChapterNumbering()) {
0388 setLocation("Chapter " + data.getChapterNumber() + " "
0389 + transform.transform(chapter.getTitle()));
0390 } else {
0391 setLocation(transform.transform(chapter.getTitle()));
0392 }
0393 final String context = getCurrentContext().getLocationWithinModule();
0394 visitor.visitEnter(chapter);
0395 if (chapter.getTitle() != null) {
0396 setLocationWithinModule(context + ".getTitle()");
0397 accept(chapter.getTitle());
0398 }
0399 if (chapter.getIntroduction() != null) {
0400 setLocationWithinModule(context + ".getIntroduction()");
0401 accept(chapter.getIntroduction());
0402 }
0403 if (chapter.getSectionList() != null) {
0404 setLocationWithinModule(context + ".getSectionList()");
0405 accept(chapter.getSectionList());
0406 }
0407 setLocationWithinModule(context);
0408 visitor.visitLeave(chapter);
0409 setLocationWithinModule(context);
0410 }
0411
0412 public void accept(final LiteratureItemList literatureItemList)
0413 throws ModuleDataException {
0414 checkForInterrupt();
0415 if (blocked || literatureItemList == null) {
0416 return;
0417 }
0418 setLocation("working on literature list");
0419 final String context = getCurrentContext().getLocationWithinModule();
0420 visitor.visitEnter(literatureItemList);
0421 for (int i = 0; i < literatureItemList.size(); i++) {
0422 setLocationWithinModule(context + ".get(" + i + ")");
0423 accept(literatureItemList.get(i));
0424 }
0425 setLocationWithinModule(context);
0426 visitor.visitLeave(literatureItemList);
0427 setLocationWithinModule(context);
0428 }
0429
0430 public void accept(final LiteratureItem item) throws ModuleDataException {
0431 checkForInterrupt();
0432 if (blocked || item == null) {
0433 return;
0434 }
0435 final String context = getCurrentContext().getLocationWithinModule();
0436 visitor.visitEnter(item);
0437 if (item.getItem() != null) {
0438 setLocationWithinModule(context + ".getItem()");
0439 accept(item.getItem());
0440 }
0441 setLocationWithinModule(context);
0442 visitor.visitLeave(item);
0443 setLocationWithinModule(context);
0444 }
0445
0446 public void accept(final SectionList sectionList) throws ModuleDataException {
0447 checkForInterrupt();
0448 if (blocked || sectionList == null) {
0449 return;
0450 }
0451 final String context = getCurrentContext().getLocationWithinModule();
0452 visitor.visitEnter(sectionList);
0453 for (int i = 0; i < sectionList.size(); i++) {
0454 setLocationWithinModule(context + ".get(" + i + ")");
0455 accept(sectionList.get(i));
0456 }
0457 setLocationWithinModule(context);
0458 visitor.visitLeave(sectionList);
0459 setLocationWithinModule(context);
0460 }
0461
0462 public void accept(final Section section) throws ModuleDataException {
0463 checkForInterrupt();
0464 if (blocked || section == null) {
0465 return;
0466 }
0467 data.increaseSectionNumber(
0468 (section.getSubsectionList() != null ? section.getSubsectionList().size() : 0),
0469 section.getNoNumber() == null || !section.getNoNumber().booleanValue()
0470 );
0471 String title = "";
0472 if (data.isChapterNumbering()) {
0473 title += data.getChapterNumber();
0474 }
0475 if (data.isSectionNumbering()) {
0476 title += (title.length() > 0 ? "." : "") + data.getSectionNumber();
0477 }
0478 if (section.getTitle() != null) {
0479 title += " " + transform.transform(section.getTitle());
0480 }
0481 location.push(title);
0482 final String context = getCurrentContext().getLocationWithinModule();
0483 visitor.visitEnter(section);
0484 if (section.getTitle() != null) {
0485 setLocationWithinModule(context + ".getTitle()");
0486 accept(section.getTitle());
0487 }
0488 if (section.getIntroduction() != null) {
0489 setLocationWithinModule(context + ".getIntroduction()");
0490 accept(section.getIntroduction());
0491 }
0492 if (section.getSubsectionList() != null) {
0493 setLocationWithinModule(context + ".getSubsectionList()");
0494 accept(section.getSubsectionList());
0495 }
0496 setLocationWithinModule(context);
0497 visitor.visitLeave(section);
0498 setLocationWithinModule(context);
0499 location.pop();
0500 }
0501
0502 public void accept(final SubsectionList subsectionList) throws ModuleDataException {
0503 checkForInterrupt();
0504 if (blocked || subsectionList == null) {
0505 return;
0506 }
0507 final String context = getCurrentContext().getLocationWithinModule();
0508 visitor.visitEnter(subsectionList);
0509 for (int i = 0; i < subsectionList.size(); i++) {
0510 setLocationWithinModule(context + ".get(" + i + ")");
0511 // TODO mime 20050608: here the Subsection context is type dependently specified
0512 // FIXME mime 20130131: variation here hard coded
0513 if (subsectionList.get(i) instanceof Subsection) {
0514 setLocationWithinModule(context + ".get(" + i + ").getSubsection()");
0515 accept((Subsection) subsectionList.get(i));
0516 } else if (subsectionList.get(i) instanceof Node) {
0517 setLocationWithinModule(context + ".get(" + i + ").getNode()");
0518 accept((Node) subsectionList.get(i));
0519 } else if (subsectionList.get(i) == null) {
0520 // ignore
0521 } else {
0522 throw new IllegalArgumentException("unexpected subsection type: "
0523 + subsectionList.get(i).getClass());
0524 }
0525 }
0526 setLocationWithinModule(context);
0527 visitor.visitLeave(subsectionList);
0528 setLocationWithinModule(context);
0529 }
0530
0531 public void accept(final Subsection subsection) throws ModuleDataException {
0532 checkForInterrupt();
0533 if (blocked || subsection == null) {
0534 return;
0535 }
0536 data.increaseSubsectionNumber();
0537 String title = "";
0538 if (data.isChapterNumbering()) {
0539 title += data.getChapterNumber();
0540 }
0541 if (data.isSectionNumbering()) {
0542 title += (title.length() > 0 ? "." : "") + data.getSectionNumber();
0543 }
0544 title += (title.length() > 0 ? "." : "") + data.getSubsectionNumber();
0545 if (subsection.getTitle() != null) {
0546 title += " " + transform.transform(subsection.getTitle());
0547 }
0548 title = title + " [" + subsection.getId() + "]";
0549 location.push(title);
0550 final String context = getCurrentContext().getLocationWithinModule();
0551 visitor.visitEnter(subsection);
0552 if (subsection.getTitle() != null) {
0553 setLocationWithinModule(context + ".getTitle()");
0554 accept(subsection.getTitle());
0555 }
0556 if (subsection.getLatex() != null) {
0557 setLocationWithinModule(context + ".getLatex()");
0558 accept(subsection.getLatex());
0559 }
0560 setLocationWithinModule(context);
0561 visitor.visitLeave(subsection);
0562 setLocationWithinModule(context);
0563 location.pop();
0564 }
0565
0566 public void accept(final Node node) throws ModuleDataException {
0567 checkForInterrupt();
0568 data.increaseNodeNumber();
0569 if (blocked || node == null) {
0570 return;
0571 }
0572 this.node = node;
0573 String title = "";
0574 if (node.getTitle() != null) {
0575 title = transform.transform(node.getTitle());
0576 }
0577 title = title + " [" + node.getId() + "]";
0578 location.push(title);
0579 final String context = getCurrentContext().getLocationWithinModule();
0580 visitor.visitEnter(node);
0581 if (node.getName() != null) {
0582 setLocationWithinModule(context + ".getName()");
0583 accept(node.getName());
0584 }
0585 if (node.getTitle() != null) {
0586 setLocationWithinModule(context + ".getTitle()");
0587 accept(node.getTitle());
0588 }
0589 if (node.getPrecedingText() != null) {
0590 setLocationWithinModule(context + ".getPrecedingText()");
0591 accept(node.getPrecedingText());
0592 }
0593 if (node.getNodeType() != null) {
0594 setLocationWithinModule(context + ".getNodeType()");
0595 if (node.getNodeType() instanceof Axiom) {
0596 setLocationWithinModule(context + ".getNodeType().getAxiom()");
0597 accept((Axiom) node.getNodeType());
0598 } else if (node.getNodeType() instanceof InitialPredicateDefinition) {
0599 setLocationWithinModule(context + ".getNodeType().getInitialPredicateDefinition()");
0600 accept((InitialPredicateDefinition) node.getNodeType());
0601 } else if (node.getNodeType() instanceof PredicateDefinition) {
0602 setLocationWithinModule(context + ".getNodeType().getPredicateDefinition()");
0603 accept((PredicateDefinition) node.getNodeType());
0604 } else if (node.getNodeType() instanceof InitialFunctionDefinition) {
0605 setLocationWithinModule(context + ".getNodeType().getInitialFunctionDefinition()");
0606 accept((InitialFunctionDefinition) node.getNodeType());
0607 } else if (node.getNodeType() instanceof FunctionDefinition) {
0608 setLocationWithinModule(context + ".getNodeType().getFunctionDefinition()");
0609 accept((FunctionDefinition) node.getNodeType());
0610 } else if (node.getNodeType() instanceof Proposition) {
0611 setLocationWithinModule(context + ".getNodeType().getProposition()");
0612 accept((Proposition) node.getNodeType());
0613 } else if (node.getNodeType() instanceof Rule) {
0614 setLocationWithinModule(context + ".getNodeType().getRule()");
0615 accept((Rule) node.getNodeType());
0616 } else {
0617 throw new IllegalArgumentException("unexpected node type: "
0618 + node.getNodeType().getClass());
0619 }
0620 }
0621 if (node.getSucceedingText() != null) {
0622 setLocationWithinModule(context + ".getSucceedingText()");
0623 accept(node.getSucceedingText());
0624 }
0625 setLocationWithinModule(context);
0626 visitor.visitLeave(node);
0627 setLocationWithinModule(context);
0628 location.pop();
0629 this.node = null;
0630 }
0631
0632 public void accept(final Axiom axiom) throws ModuleDataException {
0633 checkForInterrupt();
0634 if (blocked || axiom == null) {
0635 return;
0636 }
0637 data.increaseAxiomNumber();
0638 location.set(location.size() - 1, "Axiom " + data.getAxiomNumber() + " "
0639 + (String) location.lastElement());
0640 final String context = getCurrentContext().getLocationWithinModule();
0641 visitor.visitEnter(axiom);
0642 if (axiom.getFormula() != null) {
0643 setLocationWithinModule(context + ".getFormula()");
0644 accept(axiom.getFormula());
0645 }
0646 if (axiom.getDescription() != null) {
0647 setLocationWithinModule(context + ".getDescription()");
0648 accept(axiom.getDescription());
0649 }
0650 setLocationWithinModule(context);
0651 visitor.visitLeave(axiom);
0652 setLocationWithinModule(context);
0653 }
0654
0655 public void accept(final PredicateDefinition definition)
0656 throws ModuleDataException {
0657 checkForInterrupt();
0658 if (blocked || definition == null) {
0659 return;
0660 }
0661 data.increasePredicateDefinitionNumber();
0662 location.set(location.size() - 1, "Definition " + (data.getPredicateDefinitionNumber()
0663 + data.getFunctionDefinitionNumber()) + " "
0664 + (String) location.lastElement());
0665 final String context = getCurrentContext().getLocationWithinModule();
0666 visitor.visitEnter(definition);
0667 if (definition.getFormula() != null) {
0668 setLocationWithinModule(context + ".getFormula()");
0669 accept(definition.getFormula());
0670 }
0671 if (definition.getDescription() != null) {
0672 setLocationWithinModule(context + ".getDescription()");
0673 accept(definition.getDescription());
0674 }
0675 setLocationWithinModule(context);
0676 visitor.visitLeave(definition);
0677 setLocationWithinModule(context);
0678 }
0679
0680 public void accept(final InitialPredicateDefinition definition)
0681 throws ModuleDataException {
0682 checkForInterrupt();
0683 if (blocked || definition == null) {
0684 return;
0685 }
0686 data.increasePredicateDefinitionNumber();
0687 location.set(location.size() - 1, "Definition "
0688 + (data.getPredicateDefinitionNumber() + data
0689 .getFunctionDefinitionNumber()) + " "
0690 + (String) location.lastElement());
0691 final String context = getCurrentContext().getLocationWithinModule();
0692 visitor.visitEnter(definition);
0693 if (definition.getPredCon() != null) {
0694 setLocationWithinModule(context + ".getPredCon()");
0695 accept(definition.getPredCon());
0696 }
0697 if (definition.getDescription() != null) {
0698 setLocationWithinModule(context + ".getDescription()");
0699 accept(definition.getDescription());
0700 }
0701 setLocationWithinModule(context);
0702 visitor.visitLeave(definition);
0703 setLocationWithinModule(context);
0704 }
0705
0706 public void accept(final InitialFunctionDefinition definition) throws ModuleDataException {
0707 checkForInterrupt();
0708 if (blocked || definition == null) {
0709 return;
0710 }
0711 data.increaseFunctionDefinitionNumber();
0712 location.set(location.size() - 1, "Definition " + (data.getPredicateDefinitionNumber()
0713 + data.getFunctionDefinitionNumber()) + " "
0714 + (String) location.lastElement());
0715 final String context = getCurrentContext().getLocationWithinModule();
0716 visitor.visitEnter(definition);
0717 if (definition.getFunCon() != null) {
0718 setLocationWithinModule(context + ".getFunCon()");
0719 accept(definition.getFunCon());
0720 }
0721 if (definition.getDescription() != null) {
0722 setLocationWithinModule(context + ".getDescription()");
0723 accept(definition.getDescription());
0724 }
0725 setLocationWithinModule(context);
0726 visitor.visitLeave(definition);
0727 setLocationWithinModule(context);
0728 }
0729
0730 public void accept(final FunctionDefinition definition) throws ModuleDataException {
0731 checkForInterrupt();
0732 if (blocked || definition == null) {
0733 return;
0734 }
0735 data.increaseFunctionDefinitionNumber();
0736 location.set(location.size() - 1, "Definition " + (data.getPredicateDefinitionNumber()
0737 + data.getFunctionDefinitionNumber()) + " "
0738 + (String) location.lastElement());
0739 final String context = getCurrentContext().getLocationWithinModule();
0740 visitor.visitEnter(definition);
0741 if (definition.getFormula() != null) {
0742 setLocationWithinModule(context + ".getFormula()");
0743 accept(definition.getFormula());
0744 }
0745 if (definition.getDescription() != null) {
0746 setLocationWithinModule(context + ".getDescription()");
0747 accept(definition.getDescription());
0748 }
0749 setLocationWithinModule(context);
0750 visitor.visitLeave(definition);
0751 setLocationWithinModule(context);
0752 }
0753
0754 public void accept(final Proposition proposition) throws ModuleDataException {
0755 checkForInterrupt();
0756 if (blocked || proposition == null) {
0757 return;
0758 }
0759 data.increasePropositionNumber();
0760 location.set(location.size() - 1, "Proposition " + data.getPropositionNumber() + " "
0761 + (String) location.lastElement());
0762 final String context = getCurrentContext().getLocationWithinModule();
0763 visitor.visitEnter(proposition);
0764 if (proposition.getFormula() != null) {
0765 setLocationWithinModule(context + ".getFormula()");
0766 accept(proposition.getFormula());
0767 }
0768 if (proposition.getDescription() != null) {
0769 setLocationWithinModule(context + ".getDescription()");
0770 accept(proposition.getDescription());
0771 }
0772 if (proposition.getProofList() != null) {
0773 setLocationWithinModule(context + ".getProofList()");
0774 accept(proposition.getProofList());
0775 }
0776 if (proposition.getFormalProofList() != null) {
0777 setLocationWithinModule(context + ".getFormalProofList()");
0778 accept(proposition.getFormalProofList());
0779 }
0780 setLocationWithinModule(context);
0781 visitor.visitLeave(proposition);
0782 setLocationWithinModule(context);
0783 }
0784
0785 public void accept(final Rule rule) throws ModuleDataException {
0786 checkForInterrupt();
0787 if (blocked || rule == null) {
0788 return;
0789 }
0790 data.increaseRuleNumber();
0791 location.set(location.size() - 1, "Rule " + data.getRuleNumber() + " "
0792 + (String) location.lastElement());
0793 final String context = getCurrentContext().getLocationWithinModule();
0794 visitor.visitEnter(rule);
0795 if (rule.getLinkList() != null) {
0796 setLocationWithinModule(context + ".getLinkList()");
0797 accept(rule.getLinkList());
0798 }
0799 if (rule.getDescription() != null) {
0800 setLocationWithinModule(context + ".getDescription()");
0801 accept(rule.getDescription());
0802 }
0803 if (rule.getChangedRuleList() != null) {
0804 setLocationWithinModule(context + ".getChangedRuleList()");
0805 accept(rule.getChangedRuleList());
0806 }
0807 if (rule.getProofList() != null) {
0808 setLocationWithinModule(context + ".getProofList()");
0809 accept(rule.getProofList());
0810 }
0811 setLocationWithinModule(context);
0812 visitor.visitLeave(rule);
0813 setLocationWithinModule(context);
0814 final RuleKey newRuleKey = new RuleKey(rule.getName(), rule.getVersion());
0815 ruleExistence.put(rule.getName(), newRuleKey);
0816 }
0817
0818 public void accept(final ChangedRuleList list) throws ModuleDataException {
0819 checkForInterrupt();
0820 if (blocked || list == null) {
0821 return;
0822 }
0823 final String context = getCurrentContext().getLocationWithinModule();
0824 visitor.visitEnter(list);
0825 setLocationWithinModule(context);
0826 for (int i = 0; i < list.size(); i++) {
0827 setLocationWithinModule(context + ".get(" + i + ")");
0828 accept(list.get(i));
0829 }
0830 setLocationWithinModule(context);
0831 visitor.visitLeave(list);
0832 setLocationWithinModule(context);
0833 }
0834
0835 public void accept(final ChangedRule rule) throws ModuleDataException {
0836 checkForInterrupt();
0837 if (blocked || rule == null) {
0838 return;
0839 }
0840 data.increaseRuleNumber();
0841 location.set(location.size() - 1, "Rule " + data.getRuleNumber() + " "
0842 + (String) location.lastElement());
0843 final String context = getCurrentContext().getLocationWithinModule();
0844 visitor.visitEnter(rule);
0845 if (rule.getDescription() != null) {
0846 setLocationWithinModule(context + ".getDescription()");
0847 accept(rule.getDescription());
0848 }
0849 setLocationWithinModule(context);
0850 visitor.visitLeave(rule);
0851 setLocationWithinModule(context);
0852 final RuleKey newRuleKey = new RuleKey(rule.getName(), rule.getVersion());
0853 ruleExistence.put(rule.getName(), newRuleKey);
0854 }
0855
0856 public void accept(final LinkList linkList) throws ModuleDataException {
0857 checkForInterrupt();
0858 if (blocked || linkList == null) {
0859 return;
0860 }
0861 final String context = getCurrentContext().getLocationWithinModule();
0862 visitor.visitEnter(linkList);
0863 setLocationWithinModule(context);
0864 visitor.visitLeave(linkList);
0865 setLocationWithinModule(context);
0866 }
0867
0868 public void accept(final ProofList proofList) throws ModuleDataException {
0869 checkForInterrupt();
0870 if (blocked || proofList == null) {
0871 return;
0872 }
0873 final String context = getCurrentContext().getLocationWithinModule();
0874 visitor.visitEnter(proofList);
0875 for (int i = 0; i < proofList.size(); i++) {
0876 setLocationWithinModule(context + ".get(" + i + ")");
0877 accept(proofList.get(i));
0878 }
0879 setLocationWithinModule(context);
0880 visitor.visitLeave(proofList);
0881 setLocationWithinModule(context);
0882 }
0883
0884 public void accept(final Proof proof) throws ModuleDataException {
0885 checkForInterrupt();
0886 if (blocked || proof == null) {
0887 return;
0888 }
0889 final String context = getCurrentContext().getLocationWithinModule();
0890 visitor.visitEnter(proof);
0891 if (proof.getNonFormalProof() != null) {
0892 setLocationWithinModule(context + ".getNonFormalProof()");
0893 accept(proof.getNonFormalProof());
0894 }
0895 setLocationWithinModule(context);
0896 visitor.visitLeave(proof);
0897 setLocationWithinModule(context);
0898 }
0899
0900 public void accept(final FormalProofList proofList) throws ModuleDataException {
0901 checkForInterrupt();
0902 if (blocked || proofList == null) {
0903 return;
0904 }
0905 final String context = getCurrentContext().getLocationWithinModule();
0906 visitor.visitEnter(proofList);
0907 for (int i = 0; i < proofList.size(); i++) {
0908 setLocationWithinModule(context + ".get(" + i + ")");
0909 accept(proofList.get(i));
0910 }
0911 setLocationWithinModule(context);
0912 visitor.visitLeave(proofList);
0913 setLocationWithinModule(context);
0914 }
0915
0916 public void accept(final FormalProof proof) throws ModuleDataException {
0917 checkForInterrupt();
0918 if (blocked || proof == null) {
0919 return;
0920 }
0921 final String context = getCurrentContext().getLocationWithinModule();
0922 visitor.visitEnter(proof);
0923 if (proof.getPrecedingText() != null) {
0924 setLocationWithinModule(context + ".getPrecedingText()");
0925 accept(proof.getFormalProofLineList());
0926 }
0927 if (proof.getFormalProofLineList() != null) {
0928 setLocationWithinModule(context + ".getFormalProofLineList()");
0929 accept(proof.getFormalProofLineList());
0930 }
0931 if (proof.getSucceedingText() != null) {
0932 setLocationWithinModule(context + ".getSucceedingText()");
0933 accept(proof.getFormalProofLineList());
0934 }
0935 setLocationWithinModule(context);
0936 visitor.visitLeave(proof);
0937 setLocationWithinModule(context);
0938 }
0939
0940 public void accept(final FormalProofLineList proofLineList) throws ModuleDataException {
0941 checkForInterrupt();
0942 if (blocked || proofLineList == null) {
0943 return;
0944 }
0945 final String context = getCurrentContext().getLocationWithinModule();
0946 visitor.visitEnter(proofLineList);
0947 for (int i = 0; i < proofLineList.size(); i++) {
0948 setLocationWithinModule(context + ".get(" + i + ")");
0949 if (proofLineList.get(i) instanceof ConditionalProof) {
0950 accept((ConditionalProof) proofLineList.get(i));
0951 } else {
0952 accept(proofLineList.get(i));
0953 }
0954 }
0955 setLocationWithinModule(context);
0956 visitor.visitLeave(proofLineList);
0957 setLocationWithinModule(context);
0958 }
0959
0960 public void accept(final FormalProofLine proofLine) throws ModuleDataException {
0961 checkForInterrupt();
0962 if (blocked || proofLine == null) {
0963 return;
0964 }
0965 final String context = getCurrentContext().getLocationWithinModule();
0966 visitor.visitEnter(proofLine);
0967 if (proofLine.getFormula() != null) {
0968 setLocationWithinModule(context + ".getFormula()");
0969 accept(proofLine.getFormula());
0970 }
0971 if (proofLine.getReason() != null) {
0972 setLocationWithinModule(context + ".getReason()");
0973 accept(proofLine.getReason());
0974 }
0975 setLocationWithinModule(context);
0976 visitor.visitLeave(proofLine);
0977 setLocationWithinModule(context);
0978 }
0979
0980 public void accept(final Reason reason) throws ModuleDataException {
0981 checkForInterrupt();
0982 if (blocked || reason == null) {
0983 return;
0984 }
0985 final String context = getCurrentContext().getLocationWithinModule();
0986 visitor.visitEnter(reason);
0987 if (reason instanceof ModusPonens) {
0988 setLocationWithinModule(context + ".getModusPonens()");
0989 accept(((ModusPonens) reason).getModusPonens());
0990 } else if (reason instanceof Add) {
0991 setLocationWithinModule(context + ".getAdd()");
0992 accept(((Add) reason).getAdd());
0993 } else if (reason instanceof Rename) {
0994 setLocationWithinModule(context + ".getRename()");
0995 accept(((Rename) reason).getRename());
0996 } else if (reason instanceof SubstFree) {
0997 setLocationWithinModule(context + ".getSubstFree()");
0998 accept(((SubstFree) reason).getSubstFree());
0999 } else if (reason instanceof SubstFunc) {
1000 setLocationWithinModule(context + ".getSubstFunc()");
1001 accept(((SubstFunc) reason).getSubstFunc());
1002 } else if (reason instanceof SubstPred) {
1003 setLocationWithinModule(context + ".getSubstPred()");
1004 accept(((SubstPred) reason).getSubstPred());
1005 } else if (reason instanceof Existential) {
1006 setLocationWithinModule(context + ".getExistential()");
1007 accept(((Existential) reason).getExistential());
1008 } else if (reason instanceof Universal) {
1009 setLocationWithinModule(context + ".getUniversal()");
1010 accept(((Universal) reason).getUniversal());
1011 } else if (reason instanceof ConditionalProof) {
1012 throw new IllegalArgumentException(
1013 "proof line shall not have a conditional proof as a reason, instead the proof line "
1014 + "itself should be the conditional proof!");
1015 } else {
1016 throw new IllegalArgumentException("unexpected reason type: "
1017 + reason.getClass());
1018 }
1019 setLocationWithinModule(context);
1020 visitor.visitLeave(reason);
1021 setLocationWithinModule(context);
1022 }
1023
1024 public void accept(final ModusPonens reason) throws ModuleDataException {
1025 checkForInterrupt();
1026 if (blocked || reason == null) {
1027 return;
1028 }
1029 final String context = getCurrentContext().getLocationWithinModule();
1030 visitor.visitEnter(reason);
1031 setLocationWithinModule(context);
1032 visitor.visitLeave(reason);
1033 setLocationWithinModule(context);
1034 }
1035
1036 public void accept(final Add reason) throws ModuleDataException {
1037 checkForInterrupt();
1038 if (blocked || reason == null) {
1039 return;
1040 }
1041 final String context = getCurrentContext().getLocationWithinModule();
1042 visitor.visitEnter(reason);
1043 setLocationWithinModule(context);
1044 visitor.visitLeave(reason);
1045 setLocationWithinModule(context);
1046 }
1047
1048 public void accept(final Rename reason) throws ModuleDataException {
1049 checkForInterrupt();
1050 if (blocked || reason == null) {
1051 return;
1052 }
1053 final String context = getCurrentContext().getLocationWithinModule();
1054 visitor.visitEnter(reason);
1055 if (reason.getOriginalSubjectVariable() != null) {
1056 setLocationWithinModule(context + ".getOriginalSubjectVariable()");
1057 accept(reason.getOriginalSubjectVariable());
1058 }
1059 if (reason.getReplacementSubjectVariable() != null) {
1060 setLocationWithinModule(context + ".getReplacementSubjectVariable()");
1061 accept(reason.getReplacementSubjectVariable());
1062 }
1063 setLocationWithinModule(context);
1064 visitor.visitLeave(reason);
1065 setLocationWithinModule(context);
1066 }
1067
1068 public void accept(final SubstFree reason) throws ModuleDataException {
1069 checkForInterrupt();
1070 if (blocked || reason == null) {
1071 return;
1072 }
1073 final String context = getCurrentContext().getLocationWithinModule();
1074 visitor.visitEnter(reason);
1075 if (reason.getSubjectVariable() != null) {
1076 setLocationWithinModule(context + ".getSubjectVariable()");
1077 accept(reason.getSubjectVariable());
1078 }
1079 if (reason.getSubstituteTerm() != null) {
1080 setLocationWithinModule(context + ".getSubstituteTerm()");
1081 accept(new TermVo(reason.getSubstituteTerm()));
1082 }
1083 setLocationWithinModule(context);
1084 visitor.visitLeave(reason);
1085 setLocationWithinModule(context);
1086 }
1087
1088 public void accept(final SubstFunc reason) throws ModuleDataException {
1089 checkForInterrupt();
1090 if (blocked || reason == null) {
1091 return;
1092 }
1093 final String context = getCurrentContext().getLocationWithinModule();
1094 visitor.visitEnter(reason);
1095 if (reason.getFunctionVariable() != null) {
1096 setLocationWithinModule(context + ".getFunctionVariable()");
1097 accept(reason.getFunctionVariable());
1098 }
1099 if (reason.getSubstituteTerm() != null) {
1100 setLocationWithinModule(context + ".getSubstituteTerm()");
1101 accept(new TermVo(reason.getSubstituteTerm()));
1102 }
1103 setLocationWithinModule(context);
1104 visitor.visitLeave(reason);
1105 setLocationWithinModule(context);
1106 }
1107
1108 public void accept(final SubstPred reason) throws ModuleDataException {
1109 checkForInterrupt();
1110 if (blocked || reason == null) {
1111 return;
1112 }
1113 final String context = getCurrentContext().getLocationWithinModule();
1114 visitor.visitEnter(reason);
1115 if (reason.getPredicateVariable() != null) {
1116 setLocationWithinModule(context + ".getPredicateVariable()");
1117 accept(reason.getPredicateVariable());
1118 }
1119 if (reason.getSubstituteFormula() != null) {
1120 setLocationWithinModule(context + ".getSubstituteFormula()");
1121 accept(new FormulaVo(reason.getSubstituteFormula()));
1122 }
1123 setLocationWithinModule(context);
1124 visitor.visitLeave(reason);
1125 setLocationWithinModule(context);
1126 }
1127
1128 public void accept(final Existential reason) throws ModuleDataException {
1129 checkForInterrupt();
1130 if (blocked || reason == null) {
1131 return;
1132 }
1133 final String context = getCurrentContext().getLocationWithinModule();
1134 visitor.visitEnter(reason);
1135 if (reason.getSubjectVariable() != null) {
1136 setLocationWithinModule(context + ".getSubjectVariable()");
1137 accept(reason.getSubjectVariable());
1138 }
1139 setLocationWithinModule(context);
1140 visitor.visitLeave(reason);
1141 setLocationWithinModule(context);
1142 }
1143
1144 public void accept(final Universal reason) throws ModuleDataException {
1145 checkForInterrupt();
1146 if (blocked || reason == null) {
1147 return;
1148 }
1149 final String context = getCurrentContext().getLocationWithinModule();
1150 visitor.visitEnter(reason);
1151 if (reason.getSubjectVariable() != null) {
1152 setLocationWithinModule(context + ".getSubjectVariable()");
1153 accept(reason.getSubjectVariable());
1154 }
1155 setLocationWithinModule(context);
1156 visitor.visitLeave(reason);
1157 setLocationWithinModule(context);
1158 }
1159
1160 public void accept(final ConditionalProof reason) throws ModuleDataException {
1161 checkForInterrupt();
1162 if (blocked || reason == null) {
1163 return;
1164 }
1165 final String context = getCurrentContext().getLocationWithinModule();
1166 visitor.visitEnter(reason);
1167 if (reason.getHypothesis() != null) {
1168 setLocationWithinModule(context + ".getHypothesis()");
1169 accept(reason.getHypothesis());
1170 }
1171 if (reason.getFormalProofLineList() != null) {
1172 setLocationWithinModule(context + ".getFormalProofLineList()");
1173 accept(reason.getFormalProofLineList());
1174 }
1175 if (reason.getConclusion() != null) {
1176 setLocationWithinModule(context + ".getConclusion()");
1177 accept(reason.getConclusion());
1178 }
1179 setLocationWithinModule(context);
1180 visitor.visitLeave(reason);
1181 setLocationWithinModule(context);
1182 }
1183
1184 public void accept(final Hypothesis hypothesis) throws ModuleDataException {
1185 checkForInterrupt();
1186 if (blocked || hypothesis == null) {
1187 return;
1188 }
1189 final String context = getCurrentContext().getLocationWithinModule();
1190 visitor.visitEnter(hypothesis);
1191 if (hypothesis.getFormula() != null) {
1192 setLocationWithinModule(context + ".getFormula()");
1193 accept(hypothesis.getFormula());
1194 }
1195 setLocationWithinModule(context);
1196 visitor.visitLeave(hypothesis);
1197 setLocationWithinModule(context);
1198 }
1199
1200 public void accept(final Conclusion conclusion) throws ModuleDataException {
1201 checkForInterrupt();
1202 if (blocked || conclusion == null) {
1203 return;
1204 }
1205 final String context = getCurrentContext().getLocationWithinModule();
1206 visitor.visitEnter(conclusion);
1207 if (conclusion.getFormula() != null) {
1208 setLocationWithinModule(context + ".getFormula()");
1209 accept(conclusion.getFormula());
1210 }
1211 setLocationWithinModule(context);
1212 visitor.visitLeave(conclusion);
1213 setLocationWithinModule(context);
1214 }
1215
1216 public void accept(final Formula formula) throws ModuleDataException {
1217 checkForInterrupt();
1218 if (blocked || formula == null) {
1219 return;
1220 }
1221 final String context = getCurrentContext().getLocationWithinModule();
1222 visitor.visitEnter(formula);
1223 if (formula.getElement() != null) {
1224 setLocationWithinModule(context + ".getElement()");
1225 accept(formula.getElement());
1226 }
1227 setLocationWithinModule(context);
1228 visitor.visitLeave(formula);
1229 setLocationWithinModule(context);
1230 }
1231
1232 public void accept(final Term term) throws ModuleDataException {
1233 checkForInterrupt();
1234 if (blocked || term == null) {
1235 return;
1236 }
1237 final String context = getCurrentContext().getLocationWithinModule();
1238 visitor.visitEnter(term);
1239 if (term.getElement() != null) {
1240 setLocationWithinModule(context + ".getElement()");
1241 accept(term.getElement());
1242 }
1243 setLocationWithinModule(context);
1244 visitor.visitLeave(term);
1245 setLocationWithinModule(context);
1246 }
1247
1248 public void accept(final Element element) throws ModuleDataException {
1249 checkForInterrupt();
1250 if (blocked || element == null) {
1251 return;
1252 }
1253 final String context = getCurrentContext().getLocationWithinModule();
1254 if (element.isList()) {
1255 setLocationWithinModule(context + ".getList()");
1256 accept(element.getList());
1257 } else if (element.isAtom()) {
1258 setLocationWithinModule(context + ".getAtom()");
1259 accept(element.getAtom());
1260 } else {
1261 throw new IllegalArgumentException("unexpected element type: "
1262 + element.toString());
1263 }
1264 setLocationWithinModule(context);
1265 }
1266
1267 public void accept(final Atom atom) throws ModuleDataException {
1268 checkForInterrupt();
1269 if (blocked || atom == null) {
1270 return;
1271 }
1272 final String context = getCurrentContext().getLocationWithinModule();
1273 visitor.visitEnter(atom);
1274 setLocationWithinModule(context);
1275 visitor.visitLeave(atom);
1276 setLocationWithinModule(context);
1277 }
1278
1279 public void accept(final ElementList list) throws ModuleDataException {
1280 checkForInterrupt();
1281 if (blocked || list == null) {
1282 return;
1283 }
1284 final String context = getCurrentContext().getLocationWithinModule();
1285 visitor.visitEnter(list);
1286 for (int i = 0; i < list.size(); i++) {
1287 setLocationWithinModule(context + ".getElement(" + i + ")");
1288 accept(list.getElement(i));
1289 }
1290 setLocationWithinModule(context);
1291 visitor.visitLeave(list);
1292 setLocationWithinModule(context);
1293 }
1294
1295 public void accept(final LatexList latexList) throws ModuleDataException {
1296 checkForInterrupt();
1297 if (blocked || latexList == null) {
1298 return;
1299 }
1300 final String context = getCurrentContext().getLocationWithinModule();
1301 visitor.visitEnter(latexList);
1302 for (int i = 0; i < latexList.size(); i++) {
1303 setLocationWithinModule(context + ".get(" + i + ")");
1304 accept(latexList.get(i));
1305 }
1306 setLocationWithinModule(context);
1307 visitor.visitLeave(latexList);
1308 setLocationWithinModule(context);
1309 }
1310
1311 public void accept(final Latex latex) throws ModuleDataException {
1312 checkForInterrupt();
1313 if (blocked || latex == null) {
1314 return;
1315 }
1316 final String context = getCurrentContext().getLocationWithinModule();
1317 visitor.visitEnter(latex);
1318 setLocationWithinModule(context);
1319 visitor.visitLeave(latex);
1320 setLocationWithinModule(context);
1321 }
1322
1323 /**
1324 * Get node that is currently parsed. Might be <code>null</code>.
1325 *
1326 * @return QEDEQ node were are currently in.
1327 */
1328 public Node getNode() {
1329 return node;
1330 }
1331
1332 /**
1333 * Set location information where are we within the original module.
1334 *
1335 * @param locationWithinModule Location within module.
1336 */
1337 public void setLocationWithinModule(final String locationWithinModule) {
1338 getCurrentContext().setLocationWithinModule(locationWithinModule);
1339 }
1340
1341 public final ModuleContext getCurrentContext() {
1342 return currentContext;
1343 }
1344
1345 /**
1346 * Is further traversing blocked?
1347 *
1348 * @return Is further traversing blocked?
1349 */
1350 public final boolean getBlocked() {
1351 return blocked;
1352 }
1353
1354 /**
1355 * Set if further traverse is blocked.
1356 *
1357 * @param blocked Further transversion?
1358 */
1359 public final void setBlocked(final boolean blocked) {
1360 this.blocked = blocked;
1361 }
1362
1363 /**
1364 * Get calculated visit percentage.
1365 *
1366 * @return Value between 0 and 100.
1367 */
1368 public double getVisitPercentage() {
1369 if (data == null) {
1370 return 0;
1371 }
1372 return data.getVisitPercentage();
1373 }
1374
1375 /**
1376 * Set absolute location description.
1377 *
1378 * @param text Description.
1379 */
1380 private void setLocation(final String text) {
1381 location.setSize(0);
1382 location.push(text);
1383 }
1384 /**
1385 * Get readable description of current location.
1386 *
1387 * @return Description.
1388 */
1389 public String getLocationDescription() {
1390 final StringBuffer buffer = new StringBuffer();
1391 for (int i = 0; i < location.size(); i++) {
1392 if (i > 0) {
1393 buffer.append(" / ");
1394 }
1395 buffer.append(location.get(i));
1396 }
1397 return buffer.toString();
1398 }
1399
1400 /**
1401 * Get copy of current counters.
1402 *
1403 * @return Values of various counters.
1404 */
1405 public QedeqNumbers getCurrentNumbers() {
1406 return new QedeqNumbers(data);
1407 }
1408
1409 /**
1410 * Get current (QEDEQ module local) rule version for given rule name.
1411 *
1412 * @param name Rule name
1413 * @return Current (local) rule version. Might be <code>null</code>.
1414 */
1415 public RuleKey getLocalRuleKey(final String name) {
1416 return (RuleKey) ruleExistence.get(name);
1417 }
1418
1419 }
|