1
2
3
4
5
6
7
8
9
10
11
12
13
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
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103 public final class Context2SimpleXPath extends AbstractModuleVisitor {
104
105
106 private static final Class CLASS = Context2SimpleXPath.class;
107
108
109 private QedeqNotNullTraverser traverser;
110
111
112 private Qedeq qedeq;
113
114
115 private final ModuleContext find;
116
117
118 private SimpleXPath current;
119
120
121 private final List elements;
122
123
124 private int level;
125
126
127 private boolean matching;
128
129
130 private String matchingBegin;
131
132
133 private SimpleXPath matchingPath;
134
135
136
137
138
139
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
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
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);
192 Trace.info(CLASS, this, method, "location was not found");
193
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()")) {
275 name = null;
276 } else if (context.endsWith(".getItem()")) {
277 name = null;
278 } else {
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()")
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) {
302 enter("NAME");
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);
315 checkIfFound();
316 }
317
318 public final void visitLeave(final Latex latex) {
319
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
423
424 checkMatching(method);
425 }
426
427 public final void visitLeave(final ChapterList chapterList) {
428 traverser.setBlocked(false);
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
450
451 checkMatching(method);
452 }
453
454 public final void visitLeave(final SectionList sectionList) {
455 traverser.setBlocked(false);
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
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
561
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
588
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
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
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) {
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) {
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) {
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) {
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
968
969 checkMatching(method);
970 }
971
972 public final void visitLeave(final ChangedRuleList list) {
973 traverser.setBlocked(false);
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
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
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 {
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
1083
1084
1085
1086
1087
1088
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
1120
1121
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
1132
1133
1134
1135
1136
1137
1138
1139
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;
1149 matchingPath = new SimpleXPath(current);
1150 } else {
1151 if (context.startsWith(find.getLocationWithinModule())) {
1152
1153
1154 throw new LocationFoundException(traverser.getCurrentContext());
1155 }
1156 if (matching) {
1157
1158
1159
1160
1161
1162
1163 if (!context.startsWith(matchingBegin)) {
1164
1165
1166
1167
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
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
1184
1185
1186 current = matchingPath;
1187 throw new LocationFoundException(new ModuleContext(find.getModuleLocation(),
1188 matchingBegin));
1189 }
1190 }
1191 traverser.setBlocked(true);
1192 }
1193 checkIfFound();
1194 }
1195
1196
1197
1198
1199
1200
1201 private final void enter(final String element) {
1202 level++;
1203 current.addElement(element, addOccurence(element));
1204 }
1205
1206
1207
1208
1209 private final void leave() {
1210 level--;
1211 current.deleteLastElement();
1212 traverser.setBlocked(false);
1213 }
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
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 }