View Javadoc

1   /* This file is part of the project "Hilbert II" - http://www.qedeq.org" target="alexandria_uri">http://www.qedeq.org
2    *
3    * Copyright 2000-2014,  Michael Meyling <mime@qedeq.org>.
4    *
5    * "Hilbert II" is free software; you can redistribute
6    * it and/or modify it under the terms of the GNU General Public
7    * License as published by the Free Software Foundation; either
8    * version 2 of the License, or (at your option) any later version.
9    *
10   * This program is distributed in the hope that it will be useful,
11   * but WITHOUT ANY WARRANTY; without even the implied warranty of
12   * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13   * GNU General Public License for more details.
14   */
15  
16  package org.qedeq.kernel.xml.mapper;
17  
18  import java.util.ArrayList;
19  import java.util.HashMap;
20  import java.util.List;
21  import java.util.Map;
22  
23  import org.qedeq.base.trace.Trace;
24  import org.qedeq.base.utility.Enumerator;
25  import org.qedeq.kernel.se.base.list.ElementList;
26  import org.qedeq.kernel.se.base.module.Add;
27  import org.qedeq.kernel.se.base.module.Author;
28  import org.qedeq.kernel.se.base.module.AuthorList;
29  import org.qedeq.kernel.se.base.module.Axiom;
30  import org.qedeq.kernel.se.base.module.ChangedRule;
31  import org.qedeq.kernel.se.base.module.ChangedRuleList;
32  import org.qedeq.kernel.se.base.module.Chapter;
33  import org.qedeq.kernel.se.base.module.ChapterList;
34  import org.qedeq.kernel.se.base.module.Conclusion;
35  import org.qedeq.kernel.se.base.module.ConditionalProof;
36  import org.qedeq.kernel.se.base.module.Existential;
37  import org.qedeq.kernel.se.base.module.FormalProof;
38  import org.qedeq.kernel.se.base.module.FormalProofLine;
39  import org.qedeq.kernel.se.base.module.FormalProofLineList;
40  import org.qedeq.kernel.se.base.module.FormalProofList;
41  import org.qedeq.kernel.se.base.module.Formula;
42  import org.qedeq.kernel.se.base.module.FunctionDefinition;
43  import org.qedeq.kernel.se.base.module.Header;
44  import org.qedeq.kernel.se.base.module.Hypothesis;
45  import org.qedeq.kernel.se.base.module.Import;
46  import org.qedeq.kernel.se.base.module.ImportList;
47  import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
48  import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
49  import org.qedeq.kernel.se.base.module.Latex;
50  import org.qedeq.kernel.se.base.module.LatexList;
51  import org.qedeq.kernel.se.base.module.LinkList;
52  import org.qedeq.kernel.se.base.module.LiteratureItem;
53  import org.qedeq.kernel.se.base.module.LiteratureItemList;
54  import org.qedeq.kernel.se.base.module.Location;
55  import org.qedeq.kernel.se.base.module.LocationList;
56  import org.qedeq.kernel.se.base.module.ModusPonens;
57  import org.qedeq.kernel.se.base.module.Node;
58  import org.qedeq.kernel.se.base.module.PredicateDefinition;
59  import org.qedeq.kernel.se.base.module.Proof;
60  import org.qedeq.kernel.se.base.module.ProofList;
61  import org.qedeq.kernel.se.base.module.Proposition;
62  import org.qedeq.kernel.se.base.module.Qedeq;
63  import org.qedeq.kernel.se.base.module.Reason;
64  import org.qedeq.kernel.se.base.module.Rename;
65  import org.qedeq.kernel.se.base.module.Rule;
66  import org.qedeq.kernel.se.base.module.Section;
67  import org.qedeq.kernel.se.base.module.SectionList;
68  import org.qedeq.kernel.se.base.module.Specification;
69  import org.qedeq.kernel.se.base.module.Subsection;
70  import org.qedeq.kernel.se.base.module.SubsectionList;
71  import org.qedeq.kernel.se.base.module.SubstFree;
72  import org.qedeq.kernel.se.base.module.SubstFunc;
73  import org.qedeq.kernel.se.base.module.SubstPred;
74  import org.qedeq.kernel.se.base.module.Term;
75  import org.qedeq.kernel.se.base.module.Universal;
76  import org.qedeq.kernel.se.base.module.UsedByList;
77  import org.qedeq.kernel.se.common.ModuleContext;
78  import org.qedeq.kernel.se.common.ModuleDataException;
79  import org.qedeq.kernel.se.visitor.AbstractModuleVisitor;
80  import org.qedeq.kernel.se.visitor.QedeqNotNullTraverser;
81  import org.qedeq.kernel.xml.tracker.SimpleXPath;
82  
83  
84  /**
85   * Map content string to SimpleXPath string. This class makes it possible to transfer an location
86   * of an {@link org.qedeq.kernel.se.base.module.Qedeq} object into an XPath like position description
87   * for an XML file representation of that object.
88   *
89   * <p>
90   * See {@link #getXPath(ModuleContext, Qedeq)} for further details.
91   *
92   * <p>
93   * TODO mime 20070217: It seems to work this way but: this class assumes that we can find
94   * QEDEQ/CHAPTER[2]/SECTION[4]/SUBSECTIONS/SUBSECTION[2]
95   * even if we have some ../NODE s inbetween.
96   * (Example: NODE, NODE, SUBSECTION, NODE, SUBSECTION, NODE..)
97   *
98   * Is this still a correct XPath? (Old solution was usage of "*")
99   * Seems ok for official XPath specification, but does it work for our SimpleXPathFinder?
100  *
101  * @author  Michael Meyling
102  */
103 public final class Context2SimpleXPath extends AbstractModuleVisitor {
104 
105     /** This class. */
106     private static final Class CLASS = Context2SimpleXPath.class;
107 
108     /** Traverse QEDEQ module with this traverser. */
109     private QedeqNotNullTraverser traverser;
110 
111     /** QEDEQ object to work on. */
112     private Qedeq qedeq;
113 
114     /** Search for this context. */
115     private final ModuleContext find;
116 
117     /** We are currently at this position. */
118     private SimpleXPath current;
119 
120     /** Element stack. */
121     private final List elements;
122 
123     /** Current stack level. */
124     private int level;
125 
126     /** Is the current context already matching the beginning of the search context? */
127     private boolean matching;
128 
129     /** Last matching begin of search context. See {@link #matching}. */
130     private String matchingBegin;
131 
132     /** Corresponding XPath for the {@link #matchingBegin}. */
133     private SimpleXPath matchingPath;
134 
135     /**
136      * Constructor.
137      *
138      * @param   find    Find this location.
139      * @param   qedeq   Within this QEDEQ object.
140      */
141     private Context2SimpleXPath(final ModuleContext find, final Qedeq qedeq) {
142         this.qedeq = qedeq;
143         traverser = new QedeqNotNullTraverser(find.getModuleLocation(), this);
144         this.find = find;
145         elements = new ArrayList(20);
146     }
147 
148     /**
149      * This method finds a {@link ModuleContext} something like<br>
150      * <code>
151      * getChapterList().get(4).getSectionList().get(0).getSubsectionList().get(4).getLatex().get(0)
152      * </code><br>
153      * within a {@link Qedeq} module and returns a kind of XPath location for an associated
154      * XML document:<br>
155      * <code>QEDEQ/CHAPTER[5]/SECTION/SUBSECTIONS/SUBSECTION[2]/TEXT/LATEX</code>
156      *
157      * <p>
158      * At this example one can already see that <code>getSubsectionList().get(4)</code> is
159      * transformed into <code>SUBSECTIONS/SUBSECTION[2]</code>. This is due to the fact that
160      * <code>SUBSECTION</code> contains a sequence of <code>SUBSECTION</code> or <code>NODE</code>
161      * elements. The transformation depends not only from the context but also from
162      * the concrete QEDEQ module.
163      *
164      * <p>
165      * Especially the transformation of formula location information in their XML counterpart
166      * demands parsing the whole formula.
167      *
168      * @param   find    Find this location.
169      * @param   qedeq   Within this QEDEQ object.
170      * @return  XPath for this location in the XML document.
171      * @throws  ModuleDataException Problem with module data.
172      */
173     public static SimpleXPath getXPath(final ModuleContext find, final Qedeq qedeq)
174             throws ModuleDataException {
175         final Context2SimpleXPath converter = new Context2SimpleXPath(find, qedeq);
176         return converter.find();
177     }
178 
179     private final SimpleXPath find() throws ModuleDataException {
180         final String method = "find()";
181         Trace.paramInfo(CLASS, this, method, "find", find);
182         elements.clear();
183         level = 0;
184         current = new SimpleXPath();
185         try {
186             traverser.accept(qedeq);
187         } catch (LocationFoundException e) {
188             Trace.paramInfo(CLASS, this, method, "location found", current);
189             return current;
190         }
191         Trace.param(CLASS, this, method, "level", level);  // level should be equal to zero now
192         Trace.info(CLASS, this, method, "location was not found");
193         // do we really want to fail?
194         if (Boolean.TRUE.toString().equalsIgnoreCase(
195                 System.getProperty("qedeq.test.xmlLocationFailures"))) {
196             throw new LocationNotFoundException(traverser.getCurrentContext(),
197                 matchingBegin, find.getLocationWithinModule());
198         }
199         throw new LocationFoundException(new ModuleContext(find.getModuleLocation(),
200             matchingBegin));
201     }
202 
203     public final void visitEnter(final Qedeq qedeq) throws ModuleDataException {
204         enter("QEDEQ");
205         final String method = "visitEnter(Qedeq)";
206         Trace.param(CLASS, this, method, "current", current);
207         checkMatching(method);
208     }
209 
210     public final void visitLeave(final Qedeq qedeq) {
211         leave();
212     }
213 
214     public final void visitEnter(final Header header) throws ModuleDataException {
215         enter("HEADER");
216         final String method = "visitEnter(Header)";
217         Trace.param(CLASS, this, method, "current", current);
218         final String context = traverser.getCurrentContext().getLocationWithinModule();
219         checkMatching(method);
220 
221         traverser.setLocationWithinModule(context + ".getEmail()");
222         current.setAttribute("email");
223         checkIfFound();
224     }
225 
226     public final void visitLeave(final Header header) {
227         leave();
228     }
229 
230     public final void visitEnter(final Specification specification) throws ModuleDataException {
231         enter("SPECIFICATION");
232         final String method = "visitEnter(Specification)";
233         Trace.param(CLASS, this, method, "current", current);
234         final String context = traverser.getCurrentContext().getLocationWithinModule();
235         checkMatching(method);
236 
237         traverser.setLocationWithinModule(context + ".getName()");
238         current.setAttribute("name");
239         checkIfFound();
240 
241         traverser.setLocationWithinModule(context + ".getRuleVersion()");
242         current.setAttribute("ruleVersion");
243         checkIfFound();
244     }
245 
246     public final void visitLeave(final Specification specification) {
247         leave();
248     }
249 
250     public final void visitEnter(final LatexList latexList) throws ModuleDataException {
251         final String method = "visitEnter(LatexList)";
252         final String context = traverser.getCurrentContext().getLocationWithinModule();
253         final String name;
254         if (context.endsWith(".getTitle()")) {
255             name = "TITLE";
256         } else if (context.endsWith(".getSummary()")) {
257             name = "ABSTRACT";
258         } else if (context.endsWith(".getIntroduction()")) {
259             name = "INTRODUCTION";
260         } else if (context.endsWith(".getName()")) {
261             name = "NAME";
262         } else if (context.endsWith(".getPrecedingText()")) {
263             name = "PRECEDING";
264         } else if (context.endsWith(".getSucceedingText()")) {
265             name = "SUCCEEDING";
266         } else if (context.endsWith(".getLatex()")) {
267             name = "TEXT";
268         } else if (context.endsWith(".getDescription()")) {
269             if (context.indexOf(".getChangedRuleList().get(") >= 0) {
270                 name = null;
271             } else {
272                 name = "DESCRIPTION";
273             }
274         } else if (context.endsWith(".getNonFormalProof()")) {  // no extra XSD element
275             name = null;
276         } else if (context.endsWith(".getItem()")) {            // no extra XSD element
277             name = null;
278         } else {    // programming error
279             throw new IllegalArgumentException("unknown LatexList " + context);
280         }
281         Trace.param(CLASS, this, method, "name", name);
282         if (name != null) {
283             enter(name);
284         }
285         Trace.param(CLASS, this, method, "current", current);
286 
287         checkMatching(method);
288     }
289 
290     public final void visitLeave(final LatexList latexList) {
291         final String context = traverser.getCurrentContext().getLocationWithinModule();
292         if (!context.endsWith(".getNonFormalProof()")       // no extra XSD element
293                 && !context.endsWith(".getItem()") && !(context.endsWith(".getDescription()")
294                 && context.indexOf(".getChangedRuleList().get(") >= 0)) {
295             leave();
296         }
297     }
298 
299     public final void visitEnter(final Latex latex) throws ModuleDataException {
300         final String context = traverser.getCurrentContext().getLocationWithinModule();
301         if (context.indexOf(".getAuthorList().get(") >= 0) {    // TODO mime 20070216: why is the
302             enter("NAME");                                      // XSD so cruel???
303         }
304         enter("LATEX");
305         final String method = "visitEnter(Latex)";
306         Trace.param(CLASS, this, method, "current", current);
307         checkMatching(method);
308 
309         traverser.setLocationWithinModule(context + ".getLanguage()");
310         current.setAttribute("language");
311         checkIfFound();
312 
313         traverser.setLocationWithinModule(context + ".getLatex()");
314         current.setAttribute(null); // element character data of LATEX is LaTeX content
315         checkIfFound();
316     }
317 
318     public final void visitLeave(final Latex latex) {
319         // because NAME of AUTHOR/NAME/LATEX has no equivalent in interfaces:
320         final String context = traverser.getCurrentContext().getLocationWithinModule();
321         if (context.indexOf(".getAuthorList().get(") >= 0) {
322             leave();
323         }
324         leave();
325     }
326 
327     public final void visitEnter(final LocationList locationList) throws ModuleDataException {
328         enter("LOCATIONS");
329         final String method = "visitEnter(LocationList)";
330         Trace.param(CLASS, this, method, "current", current);
331         checkMatching(method);
332 
333     }
334 
335     public final void visitLeave(final LocationList locationList) {
336         leave();
337     }
338 
339     public final void visitEnter(final Location location) throws ModuleDataException {
340         enter("LOCATION");
341         final String method = "visitEnter(Location)";
342         Trace.param(CLASS, this, method, "current", current);
343         final String context = traverser.getCurrentContext().getLocationWithinModule();
344         checkMatching(method);
345 
346         traverser.setLocationWithinModule(context + ".getLocation()");
347         current.setAttribute("value");
348         checkIfFound();
349     }
350 
351     public final void visitLeave(final Location location) {
352         leave();
353     }
354 
355     public final void visitEnter(final AuthorList authorList) throws ModuleDataException {
356         enter("AUTHORS");
357         final String method = "visitEnter(AuthorList)";
358         Trace.param(CLASS, this, method, "current", current);
359         checkMatching(method);
360     }
361 
362     public final void visitLeave(final AuthorList authorList) {
363         leave();
364     }
365 
366     public final void visitEnter(final Author author) throws ModuleDataException {
367         enter("AUTHOR");
368         final String method = "visitEnter(Author)";
369         Trace.param(CLASS, this, method, "current", current);
370         final String context = traverser.getCurrentContext().getLocationWithinModule();
371         checkMatching(method);
372 
373         traverser.setLocationWithinModule(context + ".getEmail()");
374         current.setAttribute("email");
375         checkIfFound();
376     }
377 
378     public final void visitLeave(final Author author) {
379         leave();
380     }
381 
382     public final void visitEnter(final ImportList importList) throws ModuleDataException {
383         enter("IMPORTS");
384         final String method = "visitEnter(ImportList)";
385         Trace.param(CLASS, this, method, "current", current);
386         checkMatching(method);
387     }
388 
389     public final void visitLeave(final ImportList importList) {
390         leave();
391     }
392 
393     public final void visitEnter(final Import imp) throws ModuleDataException {
394         enter("IMPORT");
395         final String method = "visitEnter(Import)";
396         Trace.param(CLASS, this, method, "current", current);
397         final String context = traverser.getCurrentContext().getLocationWithinModule();
398         checkMatching(method);
399 
400         traverser.setLocationWithinModule(context + ".getLabel()");
401         current.setAttribute("label");
402         checkIfFound();
403     }
404 
405     public final void visitLeave(final Import imp) {
406         leave();
407     }
408 
409     public final void visitEnter(final UsedByList usedByList) throws ModuleDataException {
410         enter("USEDBY");
411         final String method = "visitEnter(UsedByList)";
412         Trace.param(CLASS, this, method, "current", current);
413         checkMatching(method);
414     }
415 
416     public final void visitLeave(final UsedByList usedByList) {
417         leave();
418     }
419 
420     public final void visitEnter(final ChapterList chapterList) throws ModuleDataException {
421         final String method = "visitEnter(ChapterList)";
422         // because no equivalent level of "getChapterList()" exists in the XSD we simply
423         // point to the current location that must be "QEDEQ"
424         checkMatching(method);
425     }
426 
427     public final void visitLeave(final ChapterList chapterList) {
428         traverser.setBlocked(false);  // free sub node search
429     }
430 
431     public final void visitEnter(final Chapter chapter) throws ModuleDataException {
432         enter("CHAPTER");
433         final String method = "visitEnter(Chapter)";
434         Trace.param(CLASS, this, method, "current", current);
435         final String context = traverser.getCurrentContext().getLocationWithinModule();
436         checkMatching(method);
437 
438         traverser.setLocationWithinModule(context + ".getNoNumber()");
439         current.setAttribute("noNumber");
440         checkIfFound();
441     }
442 
443     public final void visitLeave(final Chapter chapter) {
444         leave();
445     }
446 
447     public final void visitEnter(final SectionList sectionList) throws ModuleDataException {
448         final String method = "visitEnter(SectionList)";
449         // because no equivalent level of "getSectionList()" exists in the XSD we simply
450         // point to the current location that must be "QEDEQ/CHAPTER[x]"
451         checkMatching(method);
452     }
453 
454     public final void visitLeave(final SectionList sectionList) {
455         traverser.setBlocked(false);  // free node search again
456     }
457 
458     public final void visitEnter(final Section section) throws ModuleDataException {
459         enter("SECTION");
460         final String method = "visitEnter(Section)";
461         Trace.param(CLASS, this, method, "current", current);
462         final String context = traverser.getCurrentContext().getLocationWithinModule();
463         checkMatching(method);
464 
465         traverser.setLocationWithinModule(context + ".getNoNumber()");
466         current.setAttribute("noNumber");
467         checkIfFound();
468     }
469 
470     public final void visitLeave(final Section section) {
471         leave();
472     }
473 
474     public final void visitEnter(final SubsectionList subsectionList) throws ModuleDataException {
475         enter("SUBSECTIONS");
476         final String method = "visitEnter(SubsectionList)";
477         Trace.param(CLASS, this, method, "current", current);
478         checkMatching(method);
479     }
480 
481     public final void visitLeave(final SubsectionList subsectionList) {
482         leave();
483     }
484 
485     public final void visitEnter(final Subsection subsection) throws ModuleDataException {
486         enter("SUBSECTION");
487         final String method = "visitEnter(Subsection)";
488         Trace.param(CLASS, this, method, "current", current);
489         final String context = traverser.getCurrentContext().getLocationWithinModule();
490         checkMatching(method);
491 
492         traverser.setLocationWithinModule(context + ".getId()");
493         current.setAttribute("id");
494         checkIfFound();
495 
496         traverser.setLocationWithinModule(context + ".getLevel()");
497         current.setAttribute("level");
498         checkIfFound();
499     }
500 
501     public final void visitLeave(final Subsection subsection) {
502         leave();
503     }
504 
505     public final void visitEnter(final Node node) throws ModuleDataException {
506         enter("NODE");
507         final String method = "visitEnter(Node)";
508         Trace.param(CLASS, this, method, "current", current);
509         final String context = traverser.getCurrentContext().getLocationWithinModule();
510         checkMatching(method);
511 
512         traverser.setLocationWithinModule(context + ".getId()");
513         current.setAttribute("id");
514         checkIfFound();
515 
516         traverser.setLocationWithinModule(context + ".getLevel()");
517         current.setAttribute("level");
518         checkIfFound();
519 
520         // we dont't differentiate the different node types here and point to the parent element
521         traverser.setLocationWithinModule(context + ".getNodeType()");
522         current.setAttribute(null);
523         checkIfFound();
524 
525     }
526 
527     public final void visitLeave(final Node node) {
528         leave();
529     }
530 
531     public final void visitEnter(final Axiom axiom) throws ModuleDataException {
532         enter("AXIOM");
533         final String method = "visitEnter(Axiom)";
534         Trace.param(CLASS, this, method, "current", current);
535         final String context = traverser.getCurrentContext().getLocationWithinModule();
536         checkMatching(method);
537 
538         traverser.setLocationWithinModule(context + ".getDefinedOperator()");
539         current.setAttribute("definedOperator");
540         checkIfFound();
541     }
542 
543     public final void visitLeave(final Axiom axiom) {
544         leave();
545     }
546 
547     public final void visitEnter(final Proposition proposition) throws ModuleDataException {
548         enter("THEOREM");
549         final String method = "visitEnter(Proposition)";
550         Trace.param(CLASS, this, method, "current", current);
551         checkMatching(method);
552     }
553 
554     public final void visitLeave(final Proposition proposition) {
555         leave();
556     }
557 
558     public final void visitEnter(final ProofList proofList) throws ModuleDataException {
559         final String method = "visitEnter(ProofList)";
560         // because no equivalent level of "getProofList()" exists in the XSD we simply
561         // point to the current location that must be within the element "THEOREM" or "RULE"
562         checkMatching(method);
563     }
564 
565     public final void visitEnter(final Proof proof) throws ModuleDataException {
566         enter("PROOF");
567         final String method = "visitEnter(Proof)";
568         Trace.param(CLASS, this, method, "current", current);
569         final String context = traverser.getCurrentContext().getLocationWithinModule();
570         checkMatching(method);
571 
572         traverser.setLocationWithinModule(context + ".getKind()");
573         current.setAttribute("kind");
574         checkIfFound();
575 
576         traverser.setLocationWithinModule(context + ".getLevel()");
577         current.setAttribute("level");
578         checkIfFound();
579     }
580 
581     public final void visitLeave(final Proof proof) {
582         leave();
583     }
584 
585     public final void visitEnter(final FormalProofList proofList) throws ModuleDataException {
586         final String method = "visitEnter(FormalProofList)";
587         // because no equivalent level of "getProofList()" exists in the XSD we simply
588         // point to the current location that must be within the element "THEOREM"
589         checkMatching(method);
590     }
591 
592     public final void visitEnter(final FormalProof proof) throws ModuleDataException {
593         enter("FORMAL_PROOF");
594         final String method = "visitEnter(FormalProof)";
595         Trace.param(CLASS, this, method, "current", current);
596         checkMatching(method);
597     }
598 
599     public final void visitLeave(final FormalProof proof) {
600         leave();
601     }
602 
603     public final void visitEnter(final FormalProofLineList list) throws ModuleDataException {
604         enter("LINES");
605         final String method = "visitEnter(FormalProofLineList)";
606         Trace.param(CLASS, this, method, "current", current);
607         checkMatching(method);
608     }
609 
610     public final void visitLeave(final FormalProofLineList list) {
611         leave();
612     }
613 
614     public final void visitEnter(final FormalProofLine line) throws ModuleDataException {
615         enter("L");
616         final String method = "visitEnter(FormalProofLine)";
617         Trace.param(CLASS, this, method, "current", current);
618         final String context = traverser.getCurrentContext().getLocationWithinModule();
619         checkMatching(method);
620 
621         traverser.setLocationWithinModule(context + ".getLabel()");
622         current.setAttribute("label");
623         checkIfFound();
624     }
625 
626     public final void visitLeave(final FormalProofLine line) {
627         leave();
628     }
629 
630     public final void visitEnter(final ConditionalProof reason) throws ModuleDataException {
631         enter("CP");
632         final String method = "visitEnter(ConditionalProof)";
633         Trace.param(CLASS, this, method, "current", current);
634         checkMatching(method);
635     }
636 
637     public final void visitLeave(final ConditionalProof reason) {
638         leave();
639     }
640 
641     public final void visitEnter(final Reason reason) throws ModuleDataException {
642         // nothing to enter in XML
643         final String method = "visitEnter(Reason)";
644         Trace.param(CLASS, this, method, "current", current);
645         checkMatching(method);
646 
647     }
648 
649     public final void visitLeave(final Reason reason) {
650         // nothing to leave in XML
651     }
652 
653     public final void visitEnter(final Add reason) throws ModuleDataException {
654         enter("ADD");
655         final String method = "visitEnter(Add)";
656         Trace.param(CLASS, this, method, "current", current);
657         final String context = traverser.getCurrentContext().getLocationWithinModule();
658         checkMatching(method);
659 
660         traverser.setLocationWithinModule(context + ".getReference()");
661         current.setAttribute("ref");
662         checkIfFound();
663     }
664 
665     public final void visitLeave(final Add reason) {
666         leave();
667     }
668 
669     public final void visitEnter(final ModusPonens reason) throws ModuleDataException {
670         enter("MP");
671         final String method = "visitEnter(ModusPonens)";
672         Trace.param(CLASS, this, method, "current", current);
673         final String context = traverser.getCurrentContext().getLocationWithinModule();
674         checkMatching(method);
675 
676         traverser.setLocationWithinModule(context + ".getReference1()");
677         current.setAttribute("ref1");
678         checkIfFound();
679 
680         traverser.setLocationWithinModule(context + ".getReference2()");
681         current.setAttribute("ref2");
682         checkIfFound();
683     }
684 
685     public final void visitLeave(final ModusPonens reason) {
686         leave();
687     }
688 
689     public final void visitEnter(final Rename reason) throws ModuleDataException {
690         enter("RENAME");
691         final String method = "visitEnter(Add)";
692         Trace.param(CLASS, this, method, "current", current);
693         final String context = traverser.getCurrentContext().getLocationWithinModule();
694         checkMatching(method);
695 
696         traverser.setLocationWithinModule(context + ".getReference()");
697         current.setAttribute("ref");
698         checkIfFound();
699 
700         traverser.setLocationWithinModule(context + ".getOccurrence()");
701         current.setAttribute("occurrence");
702         checkIfFound();
703     }
704 
705     public final void visitLeave(final Rename reason) {
706         leave();
707     }
708 
709     public final void visitEnter(final SubstFree reason) throws ModuleDataException {
710         enter("SUBST_FREE");
711         final String method = "visitEnter(SubstFree)";
712         Trace.param(CLASS, this, method, "current", current);
713         final String context = traverser.getCurrentContext().getLocationWithinModule();
714         checkMatching(method);
715 
716         traverser.setLocationWithinModule(context + ".getReference()");
717         current.setAttribute("ref");
718         checkIfFound();
719     }
720 
721     public final void visitLeave(final SubstFree reason) {
722         leave();
723     }
724 
725     public final void visitEnter(final SubstFunc reason) throws ModuleDataException {
726         enter("SUBST_FUNVAR");
727         final String method = "visitEnter(SubstFunc)";
728         Trace.param(CLASS, this, method, "current", current);
729         final String context = traverser.getCurrentContext().getLocationWithinModule();
730         checkMatching(method);
731 
732         traverser.setLocationWithinModule(context + ".getReference()");
733         current.setAttribute("ref");
734         checkIfFound();
735     }
736 
737     public final void visitLeave(final SubstFunc reason) {
738         leave();
739     }
740 
741     public final void visitEnter(final SubstPred reason) throws ModuleDataException {
742         enter("SUBST_PREDVAR");
743         final String method = "visitEnter(SubstPred)";
744         Trace.param(CLASS, this, method, "current", current);
745         final String context = traverser.getCurrentContext().getLocationWithinModule();
746         checkMatching(method);
747 
748         traverser.setLocationWithinModule(context + ".getReference()");
749         current.setAttribute("ref");
750         checkIfFound();
751     }
752 
753     public final void visitLeave(final SubstPred reason) {
754         leave();
755     }
756 
757     public final void visitEnter(final Existential reason) throws ModuleDataException {
758         enter("EXISTENTIAL");
759         final String method = "visitEnter(Existential)";
760         Trace.param(CLASS, this, method, "current", current);
761         final String context = traverser.getCurrentContext().getLocationWithinModule();
762         checkMatching(method);
763 
764         traverser.setLocationWithinModule(context + ".getReference()");
765         current.setAttribute("ref");
766         checkIfFound();
767     }
768 
769     public final void visitLeave(final Existential reason) {
770         leave();
771     }
772 
773     public final void visitEnter(final Universal reason) throws ModuleDataException {
774         enter("UNIVERSAL");
775         final String method = "visitEnter(Universal)";
776         Trace.param(CLASS, this, method, "current", current);
777         final String context = traverser.getCurrentContext().getLocationWithinModule();
778         checkMatching(method);
779 
780         traverser.setLocationWithinModule(context + ".getReference()");
781         current.setAttribute("ref");
782         checkIfFound();
783     }
784 
785     public final void visitLeave(final Universal reason) {
786         leave();
787     }
788 
789     public final void visitEnter(final Hypothesis hypothesis) throws ModuleDataException {
790         enter("HYPOTHESIS");
791         final String method = "visitEnter(Hypothesis)";
792         Trace.param(CLASS, this, method, "current", current);
793         final String context = traverser.getCurrentContext().getLocationWithinModule();
794         checkMatching(method);
795 
796         traverser.setLocationWithinModule(context + ".getLabel()");
797         current.setAttribute("label");
798         checkIfFound();
799     }
800 
801     public final void visitLeave(final Hypothesis hypothesis) {
802         leave();
803     }
804 
805     public final void visitEnter(final Conclusion conclusion) throws ModuleDataException {
806         enter("CONCLUSION");
807         final String method = "visitEnter(Conclusion)";
808         Trace.param(CLASS, this, method, "current", current);
809         final String context = traverser.getCurrentContext().getLocationWithinModule();
810         checkMatching(method);
811 
812         traverser.setLocationWithinModule(context + ".getLabel()");
813         current.setAttribute("label");
814         checkIfFound();
815     }
816 
817     public final void visitLeave(final Conclusion conclusion) {
818         leave();
819     }
820 
821     public final void visitEnter(final InitialPredicateDefinition definition) throws ModuleDataException {
822         enter("DEFINITION_PREDICATE_INITIAL");
823         final String method = "visitEnter(InitialPredicateDefinition)";
824         Trace.param(CLASS, this, method, "current", current);
825         final String context = traverser.getCurrentContext().getLocationWithinModule();
826         checkMatching(method);
827 
828         traverser.setLocationWithinModule(context + ".getArgumentNumber()");
829         current.setAttribute("arguments");
830         checkIfFound();
831 
832         traverser.setLocationWithinModule(context + ".getName()");
833         current.setAttribute("name");
834         checkIfFound();
835 
836         traverser.setLocationWithinModule(context + ".getLatexPattern()");
837         enter("LATEXPATTERN");
838         if (find.getLocationWithinModule().equals(traverser.getCurrentContext()
839                 .getLocationWithinModule())) {
840             if (definition.getLatexPattern() == null) { // NOT FOUND
841                 leave();
842             }
843             throw new LocationFoundException(traverser.getCurrentContext());
844         }
845         leave();
846     }
847 
848     public final void visitLeave(final InitialPredicateDefinition definition) {
849         leave();
850     }
851 
852     public final void visitEnter(final PredicateDefinition definition) throws ModuleDataException {
853         enter("DEFINITION_PREDICATE");
854         final String method = "visitEnter(PredicateDefinition)";
855         Trace.param(CLASS, this, method, "current", current);
856         final String context = traverser.getCurrentContext().getLocationWithinModule();
857         checkMatching(method);
858 
859         traverser.setLocationWithinModule(context + ".getArgumentNumber()");
860         current.setAttribute("arguments");
861         checkIfFound();
862 
863         traverser.setLocationWithinModule(context + ".getName()");
864         current.setAttribute("name");
865         checkIfFound();
866 
867         traverser.setLocationWithinModule(context + ".getLatexPattern()");
868         enter("LATEXPATTERN");
869         if (find.getLocationWithinModule().equals(traverser.getCurrentContext()
870                 .getLocationWithinModule())) {
871             if (definition.getLatexPattern() == null) { // NOT FOUND
872                 leave();
873             }
874             throw new LocationFoundException(traverser.getCurrentContext());
875         }
876         leave();
877     }
878 
879     public final void visitLeave(final PredicateDefinition definition) {
880         leave();
881     }
882 
883     public final void visitEnter(final InitialFunctionDefinition definition) throws ModuleDataException {
884         enter("DEFINITION_FUNCTION_INITIAL");
885         final String method = "visitEnter(InitialFunctionDefinition)";
886         Trace.param(CLASS, this, method, "current", current);
887         final String context = traverser.getCurrentContext().getLocationWithinModule();
888         checkMatching(method);
889 
890         traverser.setLocationWithinModule(context + ".getArgumentNumber()");
891         current.setAttribute("arguments");
892         checkIfFound();
893 
894         traverser.setLocationWithinModule(context + ".getName()");
895         current.setAttribute("name");
896         checkIfFound();
897 
898         traverser.setLocationWithinModule(context + ".getLatexPattern()");
899         enter("LATEXPATTERN");
900         if (find.getLocationWithinModule().equals(traverser.getCurrentContext()
901                 .getLocationWithinModule())) {
902             if (definition.getLatexPattern() == null) { // NOT FOUND
903                 leave();
904             }
905             throw new LocationFoundException(traverser.getCurrentContext());
906         }
907         leave();
908     }
909 
910     public final void visitLeave(final InitialFunctionDefinition definition) {
911         leave();
912     }
913 
914     public final void visitEnter(final FunctionDefinition definition) throws ModuleDataException {
915         enter("DEFINITION_FUNCTION");
916         final String method = "visitEnter(FunctionDefinition)";
917         Trace.param(CLASS, this, method, "current", current);
918         final String context = traverser.getCurrentContext().getLocationWithinModule();
919         checkMatching(method);
920 
921         traverser.setLocationWithinModule(context + ".getArgumentNumber()");
922         current.setAttribute("arguments");
923         checkIfFound();
924 
925         traverser.setLocationWithinModule(context + ".getName()");
926         current.setAttribute("name");
927         checkIfFound();
928 
929         traverser.setLocationWithinModule(context + ".getLatexPattern()");
930         enter("LATEXPATTERN");
931         if (find.getLocationWithinModule().equals(traverser.getCurrentContext()
932                 .getLocationWithinModule())) {
933             if (definition.getLatexPattern() == null) { // NOT FOUND
934                 leave();
935             }
936             throw new LocationFoundException(traverser.getCurrentContext());
937         }
938         leave();
939     }
940 
941     public final void visitLeave(final FunctionDefinition definition) {
942         leave();
943     }
944 
945     public final void visitEnter(final Rule rule) throws ModuleDataException {
946         enter("RULE");
947         final String method = "visitEnter(Rule)";
948         Trace.param(CLASS, this, method, "current", current);
949         final String context = traverser.getCurrentContext().getLocationWithinModule();
950         checkMatching(method);
951 
952         traverser.setLocationWithinModule(context + ".getName()");
953         current.setAttribute("name");
954         checkIfFound();
955 
956         traverser.setLocationWithinModule(context + ".getVersion()");
957         current.setAttribute("version");
958         checkIfFound();
959     }
960 
961     public final void visitLeave(final Rule rule) {
962         leave();
963     }
964 
965     public final void visitEnter(final ChangedRuleList list) throws ModuleDataException {
966         final String method = "visitEnter(ChangedRuleList)";
967         // because no equivalent level of "getChangedRuleList()" exists in the XSD we simply
968         // point to the current location that must be within the element "RULE"
969         checkMatching(method);
970     }
971 
972     public final void visitLeave(final ChangedRuleList list) {
973         traverser.setBlocked(false);  // free node search again
974     }
975 
976     public final void visitEnter(final ChangedRule rule) throws ModuleDataException {
977         enter("CHANGED_RULE");
978         final String method = "visitEnter(ChangedRule)";
979         Trace.param(CLASS, this, method, "current", current);
980         final String context = traverser.getCurrentContext().getLocationWithinModule();
981         checkMatching(method);
982 
983         traverser.setLocationWithinModule(context + ".getName()");
984         current.setAttribute("name");
985         checkIfFound();
986 
987         traverser.setLocationWithinModule(context + ".getVersion()");
988         current.setAttribute("version");
989         checkIfFound();
990     }
991 
992     public final void visitLeave(final ChangedRule rule) {
993         leave();
994     }
995 
996     public final void visitEnter(final LinkList linkList) throws ModuleDataException {
997         final String method = "visitEnter(LinkList)";
998         Trace.param(CLASS, this, method, "current", current);
999         final String context = traverser.getCurrentContext().getLocationWithinModule();
1000         checkMatching(method);
1001 
1002         for (int i = 0; i < linkList.size(); i++) {
1003             enter("LINK");
1004             if (linkList.get(i) != null) {
1005                 traverser.setLocationWithinModule(context + ".get(" + i + ")");
1006                 current.setAttribute("id");
1007                 checkIfFound();
1008             }
1009             leave();
1010         };
1011     }
1012 
1013     public final void visitLeave(final LinkList linkList) {
1014         // nothing to do
1015     }
1016 
1017     public final void visitEnter(final Formula formula) throws ModuleDataException {
1018         enter("FORMULA");
1019         final String method = "visitEnter(Formula)";
1020         Trace.param(CLASS, this, method, "current", current);
1021         checkMatching(method);
1022     }
1023 
1024     public final void visitLeave(final Formula formula) {
1025         leave();
1026     }
1027 
1028     public final void visitEnter(final Term term) throws ModuleDataException {
1029         enter("TERM");
1030         final String method = "visitEnter(Term)";
1031         Trace.param(CLASS, this, method, "current", current);
1032         checkMatching(method);
1033     }
1034 
1035     public final void visitLeave(final Term term) {
1036         leave();
1037     }
1038 
1039     public final void visitEnter(final ElementList list) throws ModuleDataException {
1040         final String operator = list.getOperator();
1041         enter(operator);
1042         final String method = "visitEnter(ElementList)";
1043         Trace.param(CLASS, this, method, "current", current);
1044         String context = traverser.getCurrentContext().getLocationWithinModule();
1045 
1046         // to find something like getElement(0).getList().getElement(0)
1047         if (context.startsWith(find.getLocationWithinModule())) {
1048             throw new LocationFoundException(find);
1049         }
1050 
1051         checkMatching(method);
1052 
1053         traverser.setLocationWithinModule(context + ".getOperator()");
1054         checkIfFound();
1055         traverser.setLocationWithinModule(context);
1056         final boolean firstIsAtom = list.size() > 0 && list.getElement(0).isAtom();
1057         if (firstIsAtom) {
1058             traverser.setLocationWithinModule(context + ".getElement(0)");
1059             if ("VAR".equals(operator) || "PREDVAR".equals(operator)
1060                     || "FUNVAR".equals(operator)) {
1061                 current.setAttribute("id");
1062                 checkIfFound();
1063                 traverser.setLocationWithinModule(context + ".getElement(0).getAtom()");
1064                 checkIfFound();
1065             } else if ("PREDCON".equals(operator) || "FUNCON".equals(operator)) {
1066                 current.setAttribute("ref");
1067                 checkIfFound();
1068                 traverser.setLocationWithinModule(context + ".getElement(0).getAtom()");
1069                 checkIfFound();
1070             } else {    // should not occur, but just in case
1071                 current.setAttribute(null);
1072                 Trace.info(CLASS, this, method, "unknown operator " + operator);
1073                 throw new LocationFoundException(traverser.getCurrentContext());
1074             }
1075         }
1076     }
1077 
1078     public final void visitLeave(final ElementList list) {
1079         leave();
1080     }
1081 
1082 /* we dont need it any more
1083     public final void visitEnter(final Atom atom) throws ModuleDataException {
1084         final String method = "visitEnter(Atom)";
1085         Trace.param(this, method, "current", current);
1086         final String context = traverser.getCurrentContext().getLocationWithinModule();
1087         // mime 20070217: should never occur
1088         checkMatching(method);
1089     }
1090 */
1091     public final void visitEnter(final LiteratureItemList list) throws ModuleDataException {
1092         enter("BIBLIOGRAPHY");
1093         final String method = "visitEnter(LiteratureItemList)";
1094         Trace.param(CLASS, this, method, "current", current);
1095         checkMatching(method);
1096     }
1097 
1098     public final void visitLeave(final LiteratureItemList list) {
1099         leave();
1100     }
1101 
1102     public final void visitEnter(final LiteratureItem item) throws ModuleDataException {
1103         enter("ITEM");
1104         final String method = "visitEnter(LiteratureItem)";
1105         Trace.param(CLASS, this, method, "current", current);
1106         final String context = traverser.getCurrentContext().getLocationWithinModule();
1107         checkMatching(method);
1108 
1109         traverser.setLocationWithinModule(context + ".getLabel()");
1110         current.setAttribute("label");
1111         checkIfFound();
1112     }
1113 
1114     public final void visitLeave(final LiteratureItem item) {
1115         leave();
1116     }
1117 
1118     /**
1119      * Check if searched for context is already reached.
1120      *
1121      * @throws  LocationFoundException  We have found it.
1122      */
1123     private final void checkIfFound() throws LocationFoundException {
1124         if (find.getLocationWithinModule().equals(traverser.getCurrentContext()
1125                 .getLocationWithinModule())) {
1126             throw new LocationFoundException(traverser.getCurrentContext());
1127         }
1128     }
1129 
1130     /**
1131      * Checks if the current context matches the beginning of the context we want to find.
1132      * This method must be called at the beginning of the <code>visitEnter</code> method when
1133      * {@link #current} is correctly set. If the context of a previously visited node was already
1134      * matching and the current node doesn't start with the old matching context any longer we
1135      * throw a {@link LocationNotFoundException}.
1136      *
1137      * @param   method  Method we were called from.
1138      * @throws  LocationNotFoundException   Not found.
1139      * @throws  LocationFoundException      Success!
1140      */
1141     private final void checkMatching(final String method)
1142             throws LocationNotFoundException, LocationFoundException {
1143         final String context = traverser.getCurrentContext().getLocationWithinModule();
1144         if (find.getLocationWithinModule().startsWith(context)) {
1145             Trace.info(CLASS, this, method, "beginning matches");
1146             Trace.paramInfo(CLASS, this, method, "context", context);
1147             matching = true;
1148             matchingBegin = context;                    // remember matching context
1149             matchingPath = new SimpleXPath(current);    // remember last matching XPath
1150         } else {
1151             if (context.startsWith(find.getLocationWithinModule())) {
1152                 // our current location is more specific than our search location
1153                 // so the current location is the best match for our search
1154                 throw new LocationFoundException(traverser.getCurrentContext());
1155             }
1156             if (matching) {
1157                 // for example we are looking for "getHeader().getImportList().getImport(2)"
1158                 // getHeader()                    matches, we remember "getHeader()"
1159                 // getHeader().getSpecification() doesn't match, but still starts with "getHeader()"
1160                 // getHeader().getImportList()    matches, we remember "getHeader.getImportList()"
1161                 // getHeader().getImportList().get(0)  doesn't match but still starts with
1162                 //                                     "getHeader.getImportList()"
1163                 if (!context.startsWith(matchingBegin)) {
1164                     // Matching lost, that means we will never found the location
1165                     // so what can we do? We just return the last matching location and hope
1166                     // it is close enough to the searched one. But at least we do some
1167                     // logging here:
1168                     Trace.info(CLASS, this, method, "matching lost, when finding error location");
1169                     Trace.paramInfo(CLASS, this, method, "last match     ", matchingBegin);
1170                     Trace.paramInfo(CLASS, this, method, "current context", context);
1171                     Trace.paramInfo(CLASS, this, method, "find context   ", find.getLocationWithinModule());
1172 
1173                     Trace.traceStack(CLASS, this, method);
1174                     Trace.info(CLASS, this, method, "changing XPath to last matching one");
1175 
1176                     // do we really want to fail?
1177                     if (Boolean.TRUE.toString().equalsIgnoreCase(
1178                             System.getProperty("qedeq.test.xmlLocationFailures"))) {
1179                         throw new LocationNotFoundException(traverser.getCurrentContext(),
1180                             matchingBegin, find.getLocationWithinModule());
1181                     }
1182 
1183                     // now we change the current XPath to the last matching one because the
1184                     // contents of "current" is used as the resulting XPath later on when
1185                     // catching the exception in {@link #find()}
1186                     current = matchingPath;
1187                     throw new LocationFoundException(new ModuleContext(find.getModuleLocation(),
1188                         matchingBegin));
1189                 }
1190             }
1191             traverser.setBlocked(true);   // block further search in sub nodes
1192         }
1193         checkIfFound();
1194     }
1195 
1196     /**
1197      * Enter new XML element.
1198      *
1199      * @param   element     Element name.
1200      */
1201     private final void enter(final String element) {
1202         level++;
1203         current.addElement(element, addOccurence(element));
1204     }
1205 
1206     /**
1207      * Leave last XML element.
1208      */
1209     private final void leave() {
1210         level--;
1211         current.deleteLastElement();
1212         traverser.setBlocked(false);  //  enable further search in nodes
1213     }
1214 
1215     /**
1216      * Add element occurrence. For example we have <code>getHeader().getImportList().get(2)</code>
1217      * and we want to get <code>QEDEQ/HEADER/IMPORTS/IMPORT[3]</code>.
1218      * So we call <code>enter("QEDEQ")</code>, <code>enter("HEADER")</code>,
1219      * <code>enter("IMPORTS")</code> and last but not least
1220      * three times the sequence <code>enter("IMPORT")</code>, <code>leave("IMPORT")</code>,
1221      *
1222      * @param   name    Element that occurred.
1223      * @return  Number of occurrences including this one.
1224      */
1225     private final int addOccurence(final String name) {
1226         while (level < elements.size()) {
1227             elements.remove(elements.size() - 1);
1228         }
1229         while (level > elements.size()) {
1230             elements.add(new HashMap());
1231         }
1232         final Map levelMap = (Map) elements.get(level - 1);
1233         final Enumerator counter;
1234         if (levelMap.containsKey(name)) {
1235             counter = (Enumerator) levelMap.get(name);
1236             counter.increaseNumber();
1237         } else {
1238             counter = new Enumerator(1);
1239             levelMap.put(name, counter);
1240         }
1241         return counter.getNumber();
1242     }
1243 
1244 }