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