Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
Overview   Package   File
    FRAMES   NO FRAMES     
../../../../../img/srcFileCovDistChart10.png 0% of files have more coverage
835   1,417   299   12.28
354   1,238   0.36   68
68     4.4  
1    
 
  QedeqNotNullTraverser       Line # 91 835 299 97.7% 0.9769292
 
  (109)
 
1    /* This file is part of the project "Hilbert II" - http://www.qedeq.org
2    *
3    * Copyright 2000-2013, 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.se.visitor;
17   
18    import java.util.HashMap;
19    import java.util.Map;
20    import java.util.Stack;
21   
22    import org.qedeq.kernel.se.base.list.Atom;
23    import org.qedeq.kernel.se.base.list.Element;
24    import org.qedeq.kernel.se.base.list.ElementList;
25    import org.qedeq.kernel.se.base.module.Add;
26    import org.qedeq.kernel.se.base.module.Author;
27    import org.qedeq.kernel.se.base.module.AuthorList;
28    import org.qedeq.kernel.se.base.module.Axiom;
29    import org.qedeq.kernel.se.base.module.ChangedRule;
30    import org.qedeq.kernel.se.base.module.ChangedRuleList;
31    import org.qedeq.kernel.se.base.module.Chapter;
32    import org.qedeq.kernel.se.base.module.ChapterList;
33    import org.qedeq.kernel.se.base.module.Conclusion;
34    import org.qedeq.kernel.se.base.module.ConditionalProof;
35    import org.qedeq.kernel.se.base.module.Existential;
36    import org.qedeq.kernel.se.base.module.FormalProof;
37    import org.qedeq.kernel.se.base.module.FormalProofLine;
38    import org.qedeq.kernel.se.base.module.FormalProofLineList;
39    import org.qedeq.kernel.se.base.module.FormalProofList;
40    import org.qedeq.kernel.se.base.module.Formula;
41    import org.qedeq.kernel.se.base.module.FunctionDefinition;
42    import org.qedeq.kernel.se.base.module.Header;
43    import org.qedeq.kernel.se.base.module.Hypothesis;
44    import org.qedeq.kernel.se.base.module.Import;
45    import org.qedeq.kernel.se.base.module.ImportList;
46    import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
47    import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
48    import org.qedeq.kernel.se.base.module.Latex;
49    import org.qedeq.kernel.se.base.module.LatexList;
50    import org.qedeq.kernel.se.base.module.LinkList;
51    import org.qedeq.kernel.se.base.module.LiteratureItem;
52    import org.qedeq.kernel.se.base.module.LiteratureItemList;
53    import org.qedeq.kernel.se.base.module.Location;
54    import org.qedeq.kernel.se.base.module.LocationList;
55    import org.qedeq.kernel.se.base.module.ModusPonens;
56    import org.qedeq.kernel.se.base.module.Node;
57    import org.qedeq.kernel.se.base.module.PredicateDefinition;
58    import org.qedeq.kernel.se.base.module.Proof;
59    import org.qedeq.kernel.se.base.module.ProofList;
60    import org.qedeq.kernel.se.base.module.Proposition;
61    import org.qedeq.kernel.se.base.module.Qedeq;
62    import org.qedeq.kernel.se.base.module.Reason;
63    import org.qedeq.kernel.se.base.module.Rename;
64    import org.qedeq.kernel.se.base.module.Rule;
65    import org.qedeq.kernel.se.base.module.Section;
66    import org.qedeq.kernel.se.base.module.SectionList;
67    import org.qedeq.kernel.se.base.module.Specification;
68    import org.qedeq.kernel.se.base.module.Subsection;
69    import org.qedeq.kernel.se.base.module.SubsectionList;
70    import org.qedeq.kernel.se.base.module.SubstFree;
71    import org.qedeq.kernel.se.base.module.SubstFunc;
72    import org.qedeq.kernel.se.base.module.SubstPred;
73    import org.qedeq.kernel.se.base.module.Term;
74    import org.qedeq.kernel.se.base.module.Universal;
75    import org.qedeq.kernel.se.base.module.UsedByList;
76    import org.qedeq.kernel.se.common.ModuleAddress;
77    import org.qedeq.kernel.se.common.ModuleContext;
78    import org.qedeq.kernel.se.common.ModuleDataException;
79    import org.qedeq.kernel.se.common.RuleKey;
80    import org.qedeq.kernel.se.common.ServiceCompleteness;
81    import org.qedeq.kernel.se.dto.module.FormulaVo;
82    import org.qedeq.kernel.se.dto.module.TermVo;
83   
84   
85    /**
86    * Traverse QEDEQ module. Calls visitors of {@link org.qedeq.kernel.se.visitor.QedeqVisitor}
87    * for non <code>null</code> arguments.
88    *
89    * @author Michael Meyling
90    */
 
91    public class QedeqNotNullTraverser implements QedeqTraverser, ServiceCompleteness {
92   
93    /** Current context during creation. */
94    private final ModuleContext currentContext;
95   
96    /** Readable traverse location info. */
97    private final Stack location = new Stack();
98   
99    /** Herein are various counters for the current node. */
100    private QedeqNumbers data = new QedeqNumbers(0, 0);
101   
102    /** Converts chapter and other titles into text. */
103    private final LatexList2Text transform = new LatexList2Text();
104   
105    /**
106    * These methods are called if a node is visited. To start the whole process just call
107    * {@link #accept(Qedeq)}.
108    */
109    private QedeqVisitor visitor;
110   
111    /** Is sub node traverse currently blocked? */
112    private boolean blocked;
113   
114    /** Currently visited node element of QEDEQ module. Might be <code>null</code>. */
115    private Node node;
116   
117    /** Maps local {@link ruleName}s to local {@link RuleKey}s. */
118    private Map ruleExistence;
119   
120    /**
121    * Constructor.
122    *
123    * @param globalContext Module location information.
124    * @param visitor These methods are called if a node is visited.
125    */
 
126  68946 toggle public QedeqNotNullTraverser(final ModuleAddress globalContext, final QedeqVisitor visitor) {
127  68946 currentContext = globalContext.createModuleContext();
128  68946 this.visitor = visitor;
129    }
130   
131    /**
132    * Constructor.
133    *
134    * @param globalContext Module location information.
135    */
 
136  1 toggle public QedeqNotNullTraverser(final ModuleAddress globalContext) {
137  1 currentContext = globalContext.createModuleContext();
138    }
139   
140    /**
141    * Set visitor.
142    *
143    * @param visitor These methods are called if a node is visited.
144    */
 
145  1 toggle public void setVisitor(final QedeqVisitor visitor) {
146  1 this.visitor = visitor;
147    }
148   
 
149  68460 toggle public void accept(final Qedeq qedeq) throws ModuleDataException {
150  68460 ruleExistence = new HashMap();
151  68460 setLocation("started");
152  68460 if (qedeq == null) {
153  1 throw new NullPointerException("null QEDEQ module");
154    }
155  68459 data = new QedeqNumbers(
156  68459 (qedeq.getHeader() != null && qedeq.getHeader().getImportList() != null
157    ? qedeq.getHeader().getImportList().size() : 0),
158  68459 (qedeq.getChapterList() != null ? qedeq.getChapterList().size() : 0)
159    );
160  68459 getCurrentContext().setLocationWithinModule("");
161  68459 checkForInterrupt();
162  68459 blocked = false;
163  68459 final String context = getCurrentContext().getLocationWithinModule();
164  68459 visitor.visitEnter(qedeq);
165  68456 if (qedeq.getHeader() != null) {
166  68324 getCurrentContext().setLocationWithinModule(context + "getHeader()");
167  68324 accept(qedeq.getHeader());
168    }
169  67695 if (qedeq.getChapterList() != null) {
170  67670 getCurrentContext().setLocationWithinModule(context + "getChapterList()");
171  67670 accept(qedeq.getChapterList());
172    }
173  1893 if (qedeq.getLiteratureItemList() != null) {
174  834 getCurrentContext().setLocationWithinModule(context + "getLiteratureItemList()");
175  834 accept(qedeq.getLiteratureItemList());
176    }
177  1693 setLocationWithinModule(context);
178  1693 visitor.visitLeave(qedeq);
179  1693 setLocationWithinModule(context);
180  1693 setLocation("finished");
181  1693 data.setFinished(true);
182    }
183   
184    /**
185    * Check if current thread is interrupted.
186    *
187    * @throws InterruptException We were interrupted.
188    */
 
189  6919587 toggle private void checkForInterrupt() throws InterruptException {
190  6919587 if (Thread.interrupted()) {
191  53 throw new InterruptException(getCurrentContext());
192    }
193    }
194   
 
195  68326 toggle public void accept(final Header header) throws ModuleDataException {
196  68326 checkForInterrupt();
197  68325 if (blocked || header == null) {
198  1 return;
199    }
200  68324 setLocation("analyzing header");
201  68324 final String context = getCurrentContext().getLocationWithinModule();
202  68324 visitor.visitEnter(header);
203  68287 if (header.getSpecification() != null) {
204  68270 setLocationWithinModule(context + ".getSpecification()");
205  68270 accept(header.getSpecification());
206    }
207  68128 if (header.getTitle() != null) {
208  68110 setLocationWithinModule(context + ".getTitle()");
209  68110 accept(header.getTitle());
210    }
211  68062 if (header.getSummary() != null) {
212  68044 setLocationWithinModule(context + ".getSummary()");
213  68044 accept(header.getSummary());
214    }
215  67996 if (header.getAuthorList() != null) {
216  67979 setLocationWithinModule(context + ".getAuthorList()");
217  67979 accept(header.getAuthorList());
218    }
219  67888 if (header.getImportList() != null) {
220  26539 setLocationWithinModule(context + ".getImportList()");
221  26539 accept(header.getImportList());
222    }
223  67629 if (header.getUsedByList() != null) {
224  27515 setLocationWithinModule(context + ".getUsedByList()");
225  27515 accept(header.getUsedByList());
226    }
227  67563 setLocationWithinModule(context);
228  67563 visitor.visitLeave(header);
229  67563 setLocationWithinModule(context);
230    }
231   
 
232  27517 toggle public void accept(final UsedByList usedByList) throws ModuleDataException {
233  27517 checkForInterrupt();
234  27516 if (blocked || usedByList == null) {
235  27052 return;
236    }
237  464 location.push("working on used by list");
238  464 final String context = getCurrentContext().getLocationWithinModule();
239  464 visitor.visitEnter(usedByList);
240  849 for (int i = 0; i < usedByList.size(); i++) {
241  451 setLocationWithinModule(context + ".get(" + i + ")");
242  451 accept(usedByList.get(i));
243    }
244  398 setLocationWithinModule(context);
245  398 visitor.visitLeave(usedByList);
246  398 setLocationWithinModule(context);
247  398 location.pop();
248    }
249   
 
250  26541 toggle public void accept(final ImportList importList) throws ModuleDataException {
251  26541 checkForInterrupt();
252  26540 if (blocked || importList == null) {
253  25432 return;
254    }
255  1108 location.push("working on import list");
256  1108 final String context = getCurrentContext().getLocationWithinModule();
257  1108 visitor.visitEnter(importList);
258  2314 for (int i = 0; i < importList.size(); i++) {
259  1465 setLocationWithinModule(context + ".get(" + i + ")");
260  1465 accept(importList.get(i));
261    }
262  849 setLocationWithinModule(context);
263  849 visitor.visitLeave(importList);
264  849 setLocationWithinModule(context);
265  849 location.pop();
266    }
267   
 
268  1467 toggle public void accept(final Import imp) throws ModuleDataException {
269  1467 data.increaseImportNumber();
270  1467 checkForInterrupt();
271  1466 if (blocked || imp == null) {
272  45 return;
273    }
274  1421 location.push("import " + data.getImportNumber() + ": " + imp.getLabel());
275  1421 final String context = getCurrentContext().getLocationWithinModule();
276  1421 visitor.visitEnter(imp);
277  1312 if (imp.getSpecification() != null) {
278  1311 setLocationWithinModule(context + ".getSpecification()");
279  1311 accept(imp.getSpecification());
280    }
281  1178 setLocationWithinModule(context);
282  1178 visitor.visitLeave(imp);
283  1178 setLocationWithinModule(context);
284  1178 location.pop();
285    }
286   
 
287  70034 toggle public void accept(final Specification specification) throws ModuleDataException {
288  70034 checkForInterrupt();
289  70033 if (blocked || specification == null) {
290  66081 return;
291    }
292  3952 final String context = getCurrentContext().getLocationWithinModule();
293  3952 visitor.visitEnter(specification);
294  3816 if (specification.getLocationList() != null) {
295  3813 setLocationWithinModule(context + ".getLocationList()");
296  3813 accept(specification.getLocationList());
297    }
298  3605 setLocationWithinModule(context);
299  3605 visitor.visitLeave(specification);
300  3605 setLocationWithinModule(context);
301    }
302   
 
303  3815 toggle public void accept(final LocationList locationList) throws ModuleDataException {
304  3815 checkForInterrupt();
305  3814 if (blocked || locationList == null) {
306  566 return;
307    }
308  3248 final String context = getCurrentContext().getLocationWithinModule();
309  3248 visitor.visitEnter(locationList);
310  7046 for (int i = 0; i < locationList.size(); i++) {
311  4009 setLocationWithinModule(context + ".get(" + i + ")");
312  4009 accept(locationList.get(i));
313    }
314  3037 setLocationWithinModule(context);
315  3037 visitor.visitLeave(locationList);
316  3037 setLocationWithinModule(context);
317    }
318   
 
319  4011 toggle public void accept(final Location location) throws ModuleDataException {
320  4011 checkForInterrupt();
321  4010 if (blocked || location == null) {
322  1 return;
323    }
324  4009 final String context = getCurrentContext().getLocationWithinModule();
325  4009 visitor.visitEnter(location);
326  3868 setLocationWithinModule(context);
327  3868 visitor.visitLeave(location);
328  3868 setLocationWithinModule(context);
329    }
330   
 
331  67981 toggle public void accept(final AuthorList authorList) throws ModuleDataException {
332  67981 checkForInterrupt();
333  67980 if (blocked || authorList == null) {
334  65996 return;
335    }
336  1984 final String context = getCurrentContext().getLocationWithinModule();
337  1984 visitor.visitEnter(authorList);
338  3823 for (int i = 0; i < authorList.size(); i++) {
339  1947 setLocationWithinModule(context + ".get(" + i + ")");
340  1947 accept(authorList.get(i));
341    }
342  1876 setLocationWithinModule(context);
343  1876 visitor.visitLeave(authorList);
344  1876 setLocationWithinModule(context);
345    }
346   
 
347  1949 toggle public void accept(final Author author) throws ModuleDataException {
348  1949 checkForInterrupt();
349  1948 if (blocked || author == null) {
350  326 return;
351    }
352  1622 final String context = getCurrentContext().getLocationWithinModule();
353  1622 visitor.visitEnter(author);
354  1569 if (author.getName() != null) {
355  1568 setLocationWithinModule(context + ".getName()");
356  1568 accept(author.getName());
357    }
358  1550 setLocationWithinModule(context);
359  1550 visitor.visitLeave(author);
360  1550 setLocationWithinModule(context);
361    }
362   
 
363  67672 toggle public void accept(final ChapterList chapterList) throws ModuleDataException {
364  67672 checkForInterrupt();
365  67671 if (blocked || chapterList == null) {
366  172 return;
367    }
368  67499 final String context = getCurrentContext().getLocationWithinModule();
369  67499 visitor.visitEnter(chapterList);
370  244658 for (int i = 0; i < chapterList.size(); i++) {
371  242961 setLocationWithinModule(context + ".get(" + i + ")");
372  242961 accept(chapterList.get(i));
373    }
374  1697 setLocationWithinModule(context);
375  1697 visitor.visitLeave(chapterList);
376  1697 setLocationWithinModule(context);
377    }
378   
 
379  242963 toggle public void accept(final Chapter chapter) throws ModuleDataException {
380  242963 checkForInterrupt();
381  242962 if (blocked || chapter == null) {
382  1378 return;
383    }
384  241584 data.increaseChapterNumber(
385  241584 (chapter.getSectionList() != null ? chapter.getSectionList().size() : 0),
386    chapter.getNoNumber() == null || !chapter.getNoNumber().booleanValue()
387    );
388  241584 if (data.isChapterNumbering()) {
389  149310 setLocation("Chapter " + data.getChapterNumber() + " "
390    + transform.transform(chapter.getTitle()));
391    } else {
392  92274 setLocation(transform.transform(chapter.getTitle()));
393    }
394  241584 final String context = getCurrentContext().getLocationWithinModule();
395  241584 visitor.visitEnter(chapter);
396  241409 if (chapter.getTitle() != null) {
397  241285 setLocationWithinModule(context + ".getTitle()");
398  241285 accept(chapter.getTitle());
399    }
400  241113 if (chapter.getIntroduction() != null) {
401  240756 setLocationWithinModule(context + ".getIntroduction()");
402  240756 accept(chapter.getIntroduction());
403    }
404  240809 if (chapter.getSectionList() != null) {
405  148128 setLocationWithinModule(context + ".getSectionList()");
406  148128 accept(chapter.getSectionList());
407    }
408  175801 setLocationWithinModule(context);
409  175801 visitor.visitLeave(chapter);
410  175801 setLocationWithinModule(context);
411    }
412   
 
413  836 toggle public void accept(final LiteratureItemList literatureItemList)
414    throws ModuleDataException {
415  836 checkForInterrupt();
416  835 if (blocked || literatureItemList == null) {
417  71 return;
418    }
419  764 setLocation("working on literature list");
420  764 final String context = getCurrentContext().getLocationWithinModule();
421  764 visitor.visitEnter(literatureItemList);
422  3820 for (int i = 0; i < literatureItemList.size(); i++) {
423  3256 setLocationWithinModule(context + ".get(" + i + ")");
424  3256 accept(literatureItemList.get(i));
425    }
426  564 setLocationWithinModule(context);
427  564 visitor.visitLeave(literatureItemList);
428  564 setLocationWithinModule(context);
429    }
430   
 
431  3258 toggle public void accept(final LiteratureItem item) throws ModuleDataException {
432  3258 checkForInterrupt();
433  3257 if (blocked || item == null) {
434  1 return;
435    }
436  3256 final String context = getCurrentContext().getLocationWithinModule();
437  3256 visitor.visitEnter(item);
438  3178 if (item.getItem() != null) {
439  3177 setLocationWithinModule(context + ".getItem()");
440  3177 accept(item.getItem());
441    }
442  3064 setLocationWithinModule(context);
443  3064 visitor.visitLeave(item);
444  3064 setLocationWithinModule(context);
445    }
446   
 
447  148130 toggle public void accept(final SectionList sectionList) throws ModuleDataException {
448  148130 checkForInterrupt();
449  148129 if (blocked || sectionList == null) {
450  79675 return;
451    }
452  68454 final String context = getCurrentContext().getLocationWithinModule();
453  68454 visitor.visitEnter(sectionList);
454  202858 for (int i = 0; i < sectionList.size(); i++) {
455  199412 setLocationWithinModule(context + ".get(" + i + ")");
456  199412 accept(sectionList.get(i));
457    }
458  3446 setLocationWithinModule(context);
459  3446 visitor.visitLeave(sectionList);
460  3446 setLocationWithinModule(context);
461    }
462   
 
463  199414 toggle public void accept(final Section section) throws ModuleDataException {
464  199414 checkForInterrupt();
465  199413 if (blocked || section == null) {
466  1 return;
467    }
468  199412 data.increaseSectionNumber(
469  199412 (section.getSubsectionList() != null ? section.getSubsectionList().size() : 0),
470    section.getNoNumber() == null || !section.getNoNumber().booleanValue()
471    );
472  199412 String title = "";
473  199412 if (data.isChapterNumbering()) {
474  199412 title += data.getChapterNumber();
475    }
476  199412 if (data.isSectionNumbering()) {
477  199412 title += (title.length() > 0 ? "." : "") + data.getSectionNumber();
478    }
479  199412 if (section.getTitle() != null) {
480  199295 title += " " + transform.transform(section.getTitle());
481    }
482  199412 location.push(title);
483  199412 final String context = getCurrentContext().getLocationWithinModule();
484  199412 visitor.visitEnter(section);
485  199086 if (section.getTitle() != null) {
486  198969 setLocationWithinModule(context + ".getTitle()");
487  198969 accept(section.getTitle());
488    }
489  198457 if (section.getIntroduction() != null) {
490  198313 setLocationWithinModule(context + ".getIntroduction()");
491  198313 accept(section.getIntroduction());
492    }
493  197856 if (section.getSubsectionList() != null) {
494  182675 setLocationWithinModule(context + ".getSubsectionList()");
495  182675 accept(section.getSubsectionList());
496    }
497  134512 setLocationWithinModule(context);
498  134512 visitor.visitLeave(section);
499  134512 setLocationWithinModule(context);
500  134512 location.pop();
501    }
502   
 
503  182677 toggle public void accept(final SubsectionList subsectionList) throws ModuleDataException {
504  182677 checkForInterrupt();
505  182676 if (blocked || subsectionList == null) {
506  112756 return;
507    }
508  69920 final String context = getCurrentContext().getLocationWithinModule();
509  69920 visitor.visitEnter(subsectionList);
510  338933 for (int i = 0; i < subsectionList.size(); i++) {
511  332357 setLocationWithinModule(context + ".get(" + i + ")");
512    // TODO 20130131 m31: variation here hard coded
513    // 20050608: here the Subsection context is type dependently specified
514  332357 if (subsectionList.get(i) instanceof Subsection) {
515  8509 setLocationWithinModule(context + ".get(" + i + ").getSubsection()");
516  8509 accept((Subsection) subsectionList.get(i));
517  323848 } else if (subsectionList.get(i) instanceof Node) {
518  323848 setLocationWithinModule(context + ".get(" + i + ").getNode()");
519  323848 accept((Node) subsectionList.get(i));
520  0 } else if (subsectionList.get(i) == null) {
521    // ignore
522    } else {
523  0 throw new IllegalArgumentException("unexpected subsection type: "
524    + subsectionList.get(i).getClass());
525    }
526    }
527  6576 setLocationWithinModule(context);
528  6576 visitor.visitLeave(subsectionList);
529  6576 setLocationWithinModule(context);
530    }
531   
 
532  8511 toggle public void accept(final Subsection subsection) throws ModuleDataException {
533  8511 checkForInterrupt();
534  8510 if (blocked || subsection == null) {
535  1 return;
536    }
537  8509 data.increaseSubsectionNumber();
538  8509 String title = "";
539  8509 if (data.isChapterNumbering()) {
540  8509 title += data.getChapterNumber();
541    }
542  8509 if (data.isSectionNumbering()) {
543  8509 title += (title.length() > 0 ? "." : "") + data.getSectionNumber();
544    }
545  8509 title += (title.length() > 0 ? "." : "") + data.getSubsectionNumber();
546  8509 if (subsection.getTitle() != null) {
547  2548 title += " " + transform.transform(subsection.getTitle());
548    }
549  8509 title = title + " [" + subsection.getId() + "]";
550  8509 location.push(title);
551  8509 final String context = getCurrentContext().getLocationWithinModule();
552  8509 visitor.visitEnter(subsection);
553  8375 if (subsection.getTitle() != null) {
554  2458 setLocationWithinModule(context + ".getTitle()");
555  2458 accept(subsection.getTitle());
556    }
557  8243 if (subsection.getLatex() != null) {
558  8240 setLocationWithinModule(context + ".getLatex()");
559  8240 accept(subsection.getLatex());
560    }
561  8019 setLocationWithinModule(context);
562  8019 visitor.visitLeave(subsection);
563  8019 setLocationWithinModule(context);
564  8019 location.pop();
565    }
566   
 
567  323850 toggle public void accept(final Node node) throws ModuleDataException {
568  323850 checkForInterrupt();
569  323849 data.increaseNodeNumber();
570  323849 if (blocked || node == null) {
571  1 return;
572    }
573  323848 this.node = node;
574  323848 String title = "";
575  323848 if (node.getTitle() != null) {
576  115599 title = transform.transform(node.getTitle());
577    }
578  323848 title = title + " [" + node.getId() + "]";
579  323848 location.push(title);
580  323848 final String context = getCurrentContext().getLocationWithinModule();
581  323848 visitor.visitEnter(node);
582  321948 if (node.getName() != null) {
583  114627 setLocationWithinModule(context + ".getName()");
584  114627 accept(node.getName());
585    }
586  320914 if (node.getTitle() != null) {
587  113585 setLocationWithinModule(context + ".getTitle()");
588  113585 accept(node.getTitle());
589    }
590  319880 if (node.getPrecedingText() != null) {
591  176012 setLocationWithinModule(context + ".getPrecedingText()");
592  176012 accept(node.getPrecedingText());
593    }
594  318410 if (node.getNodeType() != null) {
595  318353 setLocationWithinModule(context + ".getNodeType()");
596  318353 if (node.getNodeType() instanceof Axiom) {
597  41137 setLocationWithinModule(context + ".getNodeType().getAxiom()");
598  41137 accept((Axiom) node.getNodeType());
599  277216 } else if (node.getNodeType() instanceof InitialPredicateDefinition) {
600  6259 setLocationWithinModule(context + ".getNodeType().getInitialPredicateDefinition()");
601  6259 accept((InitialPredicateDefinition) node.getNodeType());
602  270957 } else if (node.getNodeType() instanceof PredicateDefinition) {
603  19768 setLocationWithinModule(context + ".getNodeType().getPredicateDefinition()");
604  19768 accept((PredicateDefinition) node.getNodeType());
605  251189 } else if (node.getNodeType() instanceof InitialFunctionDefinition) {
606  5 setLocationWithinModule(context + ".getNodeType().getInitialFunctionDefinition()");
607  5 accept((InitialFunctionDefinition) node.getNodeType());
608  251184 } else if (node.getNodeType() instanceof FunctionDefinition) {
609  27370 setLocationWithinModule(context + ".getNodeType().getFunctionDefinition()");
610  27370 accept((FunctionDefinition) node.getNodeType());
611  223814 } else if (node.getNodeType() instanceof Proposition) {
612  211080 setLocationWithinModule(context + ".getNodeType().getProposition()");
613  211080 accept((Proposition) node.getNodeType());
614  12734 } else if (node.getNodeType() instanceof Rule) {
615  12734 setLocationWithinModule(context + ".getNodeType().getRule()");
616  12734 accept((Rule) node.getNodeType());
617    } else {
618  0 throw new IllegalArgumentException("unexpected node type: "
619    + node.getNodeType().getClass());
620    }
621    }
622  261520 if (node.getSucceedingText() != null) {
623  45924 setLocationWithinModule(context + ".getSucceedingText()");
624  45924 accept(node.getSucceedingText());
625    }
626  261160 setLocationWithinModule(context);
627  261160 visitor.visitLeave(node);
628  261160 setLocationWithinModule(context);
629  261160 location.pop();
630  261160 this.node = null;
631    }
632   
 
633  41139 toggle public void accept(final Axiom axiom) throws ModuleDataException {
634  41139 checkForInterrupt();
635  41138 if (blocked || axiom == null) {
636  28743 return;
637    }
638  12395 data.increaseAxiomNumber();
639  12395 location.set(location.size() - 1, "Axiom " + data.getAxiomNumber() + " "
640    + (String) location.lastElement());
641  12395 final String context = getCurrentContext().getLocationWithinModule();
642  12395 visitor.visitEnter(axiom);
643  12191 if (axiom.getFormula() != null) {
644  12188 setLocationWithinModule(context + ".getFormula()");
645  12188 accept(axiom.getFormula());
646    }
647  8317 if (axiom.getDescription() != null) {
648  2 setLocationWithinModule(context + ".getDescription()");
649  2 accept(axiom.getDescription());
650    }
651  8317 setLocationWithinModule(context);
652  8317 visitor.visitLeave(axiom);
653  8317 setLocationWithinModule(context);
654    }
655   
 
656  19770 toggle public void accept(final PredicateDefinition definition)
657    throws ModuleDataException {
658  19770 checkForInterrupt();
659  19769 if (blocked || definition == null) {
660  16080 return;
661    }
662  3689 data.increasePredicateDefinitionNumber();
663  3689 location.set(location.size() - 1, "Definition " + (data.getPredicateDefinitionNumber()
664    + data.getFunctionDefinitionNumber()) + " "
665    + (String) location.lastElement());
666  3689 final String context = getCurrentContext().getLocationWithinModule();
667  3689 visitor.visitEnter(definition);
668  3572 if (definition.getFormula() != null) {
669  3569 setLocationWithinModule(context + ".getFormula()");
670  3569 accept(definition.getFormula());
671    }
672  2488 if (definition.getDescription() != null) {
673  2 setLocationWithinModule(context + ".getDescription()");
674  2 accept(definition.getDescription());
675    }
676  2488 setLocationWithinModule(context);
677  2488 visitor.visitLeave(definition);
678  2488 setLocationWithinModule(context);
679    }
680   
 
681  6261 toggle public void accept(final InitialPredicateDefinition definition)
682    throws ModuleDataException {
683  6261 checkForInterrupt();
684  6260 if (blocked || definition == null) {
685  5305 return;
686    }
687  955 data.increasePredicateDefinitionNumber();
688  955 location.set(location.size() - 1, "Definition "
689    + (data.getPredicateDefinitionNumber() + data
690    .getFunctionDefinitionNumber()) + " "
691    + (String) location.lastElement());
692  955 final String context = getCurrentContext().getLocationWithinModule();
693  955 visitor.visitEnter(definition);
694  906 if (definition.getPredCon() != null) {
695  903 setLocationWithinModule(context + ".getPredCon()");
696  903 accept(definition.getPredCon());
697    }
698  810 if (definition.getDescription() != null) {
699  2 setLocationWithinModule(context + ".getDescription()");
700  2 accept(definition.getDescription());
701    }
702  810 setLocationWithinModule(context);
703  810 visitor.visitLeave(definition);
704  810 setLocationWithinModule(context);
705    }
706   
 
707  7 toggle public void accept(final InitialFunctionDefinition definition) throws ModuleDataException {
708  7 checkForInterrupt();
709  6 if (blocked || definition == null) {
710  1 return;
711    }
712  5 data.increaseFunctionDefinitionNumber();
713  5 location.set(location.size() - 1, "Definition " + (data.getPredicateDefinitionNumber()
714    + data.getFunctionDefinitionNumber()) + " "
715    + (String) location.lastElement());
716  5 final String context = getCurrentContext().getLocationWithinModule();
717  5 visitor.visitEnter(definition);
718  5 if (definition.getFunCon() != null) {
719  2 setLocationWithinModule(context + ".getFunCon()");
720  2 accept(definition.getFunCon());
721    }
722  5 if (definition.getDescription() != null) {
723  2 setLocationWithinModule(context + ".getDescription()");
724  2 accept(definition.getDescription());
725    }
726  5 setLocationWithinModule(context);
727  5 visitor.visitLeave(definition);
728  5 setLocationWithinModule(context);
729    }
730   
 
731  27372 toggle public void accept(final FunctionDefinition definition) throws ModuleDataException {
732  27372 checkForInterrupt();
733  27371 if (blocked || definition == null) {
734  20981 return;
735    }
736  6390 data.increaseFunctionDefinitionNumber();
737  6390 location.set(location.size() - 1, "Definition " + (data.getPredicateDefinitionNumber()
738    + data.getFunctionDefinitionNumber()) + " "
739    + (String) location.lastElement());
740  6390 final String context = getCurrentContext().getLocationWithinModule();
741  6390 visitor.visitEnter(definition);
742  6190 if (definition.getFormula() != null) {
743  6187 setLocationWithinModule(context + ".getFormula()");
744  6187 accept(definition.getFormula());
745    }
746  4055 if (definition.getDescription() != null) {
747  2 setLocationWithinModule(context + ".getDescription()");
748  2 accept(definition.getDescription());
749    }
750  4055 setLocationWithinModule(context);
751  4055 visitor.visitLeave(definition);
752  4055 setLocationWithinModule(context);
753    }
754   
 
755  211082 toggle public void accept(final Proposition proposition) throws ModuleDataException {
756  211082 checkForInterrupt();
757  211081 if (blocked || proposition == null) {
758  145289 return;
759    }
760  65792 data.increasePropositionNumber();
761  65792 location.set(location.size() - 1, "Proposition " + data.getPropositionNumber() + " "
762    + (String) location.lastElement());
763  65792 final String context = getCurrentContext().getLocationWithinModule();
764  65792 visitor.visitEnter(proposition);
765  65340 if (proposition.getFormula() != null) {
766  65285 setLocationWithinModule(context + ".getFormula()");
767  65285 accept(proposition.getFormula());
768    }
769  44869 if (proposition.getDescription() != null) {
770  310 setLocationWithinModule(context + ".getDescription()");
771  310 accept(proposition.getDescription());
772    }
773  44855 if (proposition.getProofList() != null) {
774  4966 setLocationWithinModule(context + ".getProofList()");
775  4966 accept(proposition.getProofList());
776    }
777  44242 if (proposition.getFormalProofList() != null) {
778  29461 setLocationWithinModule(context + ".getFormalProofList()");
779  29461 accept(proposition.getFormalProofList());
780    }
781  17260 setLocationWithinModule(context);
782  17260 visitor.visitLeave(proposition);
783  17260 setLocationWithinModule(context);
784    }
785   
 
786  12736 toggle public void accept(final Rule rule) throws ModuleDataException {
787  12736 checkForInterrupt();
788  12735 if (blocked || rule == null) {
789  6337 return;
790    }
791  6398 data.increaseRuleNumber();
792  6398 location.set(location.size() - 1, "Rule " + data.getRuleNumber() + " "
793    + (String) location.lastElement());
794  6398 final String context = getCurrentContext().getLocationWithinModule();
795  6398 visitor.visitEnter(rule);
796  6134 if (rule.getLinkList() != null) {
797  479 setLocationWithinModule(context + ".getLinkList()");
798  479 accept(rule.getLinkList());
799    }
800  6122 if (rule.getDescription() != null) {
801  6112 setLocationWithinModule(context + ".getDescription()");
802  6112 accept(rule.getDescription());
803    }
804  5876 if (rule.getChangedRuleList() != null) {
805  128 setLocationWithinModule(context + ".getChangedRuleList()");
806  128 accept(rule.getChangedRuleList());
807    }
808  5810 if (rule.getProofList() != null) {
809  62 setLocationWithinModule(context + ".getProofList()");
810  62 accept(rule.getProofList());
811    }
812  5799 setLocationWithinModule(context);
813  5799 visitor.visitLeave(rule);
814  5799 setLocationWithinModule(context);
815  5799 final RuleKey newRuleKey = new RuleKey(rule.getName(), rule.getVersion());
816  5799 ruleExistence.put(rule.getName(), newRuleKey);
817    }
818   
 
819  130 toggle public void accept(final ChangedRuleList list) throws ModuleDataException {
820  130 checkForInterrupt();
821  129 if (blocked || list == null) {
822  22 return;
823    }
824  107 final String context = getCurrentContext().getLocationWithinModule();
825  107 visitor.visitEnter(list);
826  105 setLocationWithinModule(context);
827  628 for (int i = 0; i < list.size(); i++) {
828  587 setLocationWithinModule(context + ".get(" + i + ")");
829  587 accept(list.get(i));
830    }
831  41 setLocationWithinModule(context);
832  41 visitor.visitLeave(list);
833  41 setLocationWithinModule(context);
834    }
835   
 
836  589 toggle public void accept(final ChangedRule rule) throws ModuleDataException {
837  589 checkForInterrupt();
838  588 if (blocked || rule == null) {
839  89 return;
840    }
841  499 data.increaseRuleNumber();
842  499 location.set(location.size() - 1, "Rule " + data.getRuleNumber() + " "
843    + (String) location.lastElement());
844  499 final String context = getCurrentContext().getLocationWithinModule();
845  499 visitor.visitEnter(rule);
846  467 if (rule.getDescription() != null) {
847  466 setLocationWithinModule(context + ".getDescription()");
848  466 accept(rule.getDescription());
849    }
850  435 setLocationWithinModule(context);
851  435 visitor.visitLeave(rule);
852  435 setLocationWithinModule(context);
853  435 final RuleKey newRuleKey = new RuleKey(rule.getName(), rule.getVersion());
854  435 ruleExistence.put(rule.getName(), newRuleKey);
855    }
856   
 
857  481 toggle public void accept(final LinkList linkList) throws ModuleDataException {
858  481 checkForInterrupt();
859  480 if (blocked || linkList == null) {
860  301 return;
861    }
862  179 final String context = getCurrentContext().getLocationWithinModule();
863  179 visitor.visitEnter(linkList);
864  167 setLocationWithinModule(context);
865  167 visitor.visitLeave(linkList);
866  167 setLocationWithinModule(context);
867    }
868   
 
869  5030 toggle public void accept(final ProofList proofList) throws ModuleDataException {
870  5030 checkForInterrupt();
871  5029 if (blocked || proofList == null) {
872  3994 return;
873    }
874  1035 final String context = getCurrentContext().getLocationWithinModule();
875  1035 visitor.visitEnter(proofList);
876  1379 for (int i = 0; i < proofList.size(); i++) {
877  968 setLocationWithinModule(context + ".get(" + i + ")");
878  968 accept(proofList.get(i));
879    }
880  411 setLocationWithinModule(context);
881  411 visitor.visitLeave(proofList);
882  411 setLocationWithinModule(context);
883    }
884   
 
885  970 toggle public void accept(final Proof proof) throws ModuleDataException {
886  970 checkForInterrupt();
887  969 if (blocked || proof == null) {
888  1 return;
889    }
890  968 final String context = getCurrentContext().getLocationWithinModule();
891  968 visitor.visitEnter(proof);
892  732 if (proof.getNonFormalProof() != null) {
893  730 setLocationWithinModule(context + ".getNonFormalProof()");
894  730 accept(proof.getNonFormalProof());
895    }
896  454 setLocationWithinModule(context);
897  454 visitor.visitLeave(proof);
898  454 setLocationWithinModule(context);
899    }
900   
 
901  29463 toggle public void accept(final FormalProofList proofList) throws ModuleDataException {
902  29463 checkForInterrupt();
903  29462 if (blocked || proofList == null) {
904  1128 return;
905    }
906  28334 final String context = getCurrentContext().getLocationWithinModule();
907  28334 visitor.visitEnter(proofList);
908  29581 for (int i = 0; i < proofList.size(); i++) {
909  28229 setLocationWithinModule(context + ".get(" + i + ")");
910  28229 accept(proofList.get(i));
911    }
912  1352 setLocationWithinModule(context);
913  1352 visitor.visitLeave(proofList);
914  1352 setLocationWithinModule(context);
915    }
916   
 
917  28231 toggle public void accept(final FormalProof proof) throws ModuleDataException {
918  28231 checkForInterrupt();
919  28230 if (blocked || proof == null) {
920  1 return;
921    }
922  28229 final String context = getCurrentContext().getLocationWithinModule();
923  28229 visitor.visitEnter(proof);
924  28073 if (proof.getPrecedingText() != null) {
925  2 setLocationWithinModule(context + ".getPrecedingText()");
926  2 accept(proof.getFormalProofLineList());
927    }
928  28073 if (proof.getFormalProofLineList() != null) {
929  28068 setLocationWithinModule(context + ".getFormalProofLineList()");
930  28068 accept(proof.getFormalProofLineList());
931    }
932  1351 if (proof.getSucceedingText() != null) {
933  2 setLocationWithinModule(context + ".getSucceedingText()");
934  2 accept(proof.getFormalProofLineList());
935    }
936  1351 setLocationWithinModule(context);
937  1351 visitor.visitLeave(proof);
938  1351 setLocationWithinModule(context);
939    }
940   
 
941  41602 toggle public void accept(final FormalProofLineList proofLineList) throws ModuleDataException {
942  41602 checkForInterrupt();
943  41601 if (blocked || proofLineList == null) {
944  6217 return;
945    }
946  35384 final String context = getCurrentContext().getLocationWithinModule();
947  35384 visitor.visitEnter(proofLineList);
948  238858 for (int i = 0; i < proofLineList.size(); i++) {
949  234550 setLocationWithinModule(context + ".get(" + i + ")");
950  234550 if (proofLineList.get(i) instanceof ConditionalProof) {
951  14607 accept((ConditionalProof) proofLineList.get(i));
952    } else {
953  219943 accept(proofLineList.get(i));
954    }
955    }
956  4308 setLocationWithinModule(context);
957  4308 visitor.visitLeave(proofLineList);
958  4308 setLocationWithinModule(context);
959    }
960   
 
961  219945 toggle public void accept(final FormalProofLine proofLine) throws ModuleDataException {
962  219945 checkForInterrupt();
963  219944 if (blocked || proofLine == null) {
964  3469 return;
965    }
966  216475 final String context = getCurrentContext().getLocationWithinModule();
967  216475 visitor.visitEnter(proofLine);
968  214845 if (proofLine.getFormula() != null) {
969  214816 setLocationWithinModule(context + ".getFormula()");
970  214816 accept(proofLine.getFormula());
971    }
972  193498 if (proofLine.getReason() != null) {
973  193494 setLocationWithinModule(context + ".getReason()");
974  193494 accept(proofLine.getReason());
975    }
976  191819 setLocationWithinModule(context);
977  191819 visitor.visitLeave(proofLine);
978  191819 setLocationWithinModule(context);
979    }
980   
 
981  193496 toggle public void accept(final Reason reason) throws ModuleDataException {
982  193496 checkForInterrupt();
983  193495 if (blocked || reason == null) {
984  178393 return;
985    }
986  15102 final String context = getCurrentContext().getLocationWithinModule();
987  15102 visitor.visitEnter(reason);
988  14028 if (reason instanceof ModusPonens) {
989  3980 setLocationWithinModule(context + ".getModusPonens()");
990  3980 accept(((ModusPonens) reason).getModusPonens());
991  10048 } else if (reason instanceof Add) {
992  3148 setLocationWithinModule(context + ".getAdd()");
993  3148 accept(((Add) reason).getAdd());
994  6900 } else if (reason instanceof Rename) {
995  656 setLocationWithinModule(context + ".getRename()");
996  656 accept(((Rename) reason).getRename());
997  6244 } else if (reason instanceof SubstFree) {
998  386 setLocationWithinModule(context + ".getSubstFree()");
999  386 accept(((SubstFree) reason).getSubstFree());
1000  5858 } else if (reason instanceof SubstFunc) {
1001  122 setLocationWithinModule(context + ".getSubstFunc()");
1002  122 accept(((SubstFunc) reason).getSubstFunc());
1003  5736 } else if (reason instanceof SubstPred) {
1004  5345 setLocationWithinModule(context + ".getSubstPred()");
1005  5345 accept(((SubstPred) reason).getSubstPred());
1006  391 } else if (reason instanceof Existential) {
1007  80 setLocationWithinModule(context + ".getExistential()");
1008  80 accept(((Existential) reason).getExistential());
1009  311 } else if (reason instanceof Universal) {
1010  311 setLocationWithinModule(context + ".getUniversal()");
1011  311 accept(((Universal) reason).getUniversal());
1012  0 } else if (reason instanceof ConditionalProof) {
1013  0 throw new IllegalArgumentException(
1014    "proof line shall not have a conditional proof as a reason, instead the proof line "
1015    + "itself should be the conditional proof!");
1016    } else {
1017  0 throw new IllegalArgumentException("unexpected reason type: "
1018    + reason.getClass());
1019    }
1020  13423 setLocationWithinModule(context);
1021  13423 visitor.visitLeave(reason);
1022  13423 setLocationWithinModule(context);
1023    }
1024   
 
1025  3982 toggle public void accept(final ModusPonens reason) throws ModuleDataException {
1026  3982 checkForInterrupt();
1027  3981 if (blocked || reason == null) {
1028  1 return;
1029    }
1030  3980 final String context = getCurrentContext().getLocationWithinModule();
1031  3980 visitor.visitEnter(reason);
1032  3805 setLocationWithinModule(context);
1033  3805 visitor.visitLeave(reason);
1034  3805 setLocationWithinModule(context);
1035    }
1036   
 
1037  3150 toggle public void accept(final Add reason) throws ModuleDataException {
1038  3150 checkForInterrupt();
1039  3149 if (blocked || reason == null) {
1040  1 return;
1041    }
1042  3148 final String context = getCurrentContext().getLocationWithinModule();
1043  3148 visitor.visitEnter(reason);
1044  3011 setLocationWithinModule(context);
1045  3011 visitor.visitLeave(reason);
1046  3011 setLocationWithinModule(context);
1047    }
1048   
 
1049  658 toggle public void accept(final Rename reason) throws ModuleDataException {
1050  658 checkForInterrupt();
1051  657 if (blocked || reason == null) {
1052  1 return;
1053    }
1054  656 final String context = getCurrentContext().getLocationWithinModule();
1055  656 visitor.visitEnter(reason);
1056  627 if (reason.getOriginalSubjectVariable() != null) {
1057  552 setLocationWithinModule(context + ".getOriginalSubjectVariable()");
1058  552 accept(reason.getOriginalSubjectVariable());
1059    }
1060  627 if (reason.getReplacementSubjectVariable() != null) {
1061  504 setLocationWithinModule(context + ".getReplacementSubjectVariable()");
1062  504 accept(reason.getReplacementSubjectVariable());
1063    }
1064  627 setLocationWithinModule(context);
1065  627 visitor.visitLeave(reason);
1066  627 setLocationWithinModule(context);
1067    }
1068   
 
1069  388 toggle public void accept(final SubstFree reason) throws ModuleDataException {
1070  388 checkForInterrupt();
1071  387 if (blocked || reason == null) {
1072  1 return;
1073    }
1074  386 final String context = getCurrentContext().getLocationWithinModule();
1075  386 visitor.visitEnter(reason);
1076  370 if (reason.getSubjectVariable() != null) {
1077  271 setLocationWithinModule(context + ".getSubjectVariable()");
1078  271 accept(reason.getSubjectVariable());
1079    }
1080  370 if (reason.getSubstituteTerm() != null) {
1081  343 setLocationWithinModule(context + ".getSubstituteTerm()");
1082  343 accept(new TermVo(reason.getSubstituteTerm()));
1083    }
1084  370 setLocationWithinModule(context);
1085  370 visitor.visitLeave(reason);
1086  370 setLocationWithinModule(context);
1087    }
1088   
 
1089  124 toggle public void accept(final SubstFunc reason) throws ModuleDataException {
1090  124 checkForInterrupt();
1091  123 if (blocked || reason == null) {
1092  1 return;
1093    }
1094  122 final String context = getCurrentContext().getLocationWithinModule();
1095  122 visitor.visitEnter(reason);
1096  116 if (reason.getFunctionVariable() != null) {
1097  65 setLocationWithinModule(context + ".getFunctionVariable()");
1098  65 accept(reason.getFunctionVariable());
1099    }
1100  116 if (reason.getSubstituteTerm() != null) {
1101  89 setLocationWithinModule(context + ".getSubstituteTerm()");
1102  89 accept(new TermVo(reason.getSubstituteTerm()));
1103    }
1104  116 setLocationWithinModule(context);
1105  116 visitor.visitLeave(reason);
1106  116 setLocationWithinModule(context);
1107    }
1108   
 
1109  5347 toggle public void accept(final SubstPred reason) throws ModuleDataException {
1110  5347 checkForInterrupt();
1111  5346 if (blocked || reason == null) {
1112  1 return;
1113    }
1114  5345 final String context = getCurrentContext().getLocationWithinModule();
1115  5345 visitor.visitEnter(reason);
1116  5119 if (reason.getPredicateVariable() != null) {
1117  4900 setLocationWithinModule(context + ".getPredicateVariable()");
1118  4900 accept(reason.getPredicateVariable());
1119    }
1120  5119 if (reason.getSubstituteFormula() != null) {
1121  4900 setLocationWithinModule(context + ".getSubstituteFormula()");
1122  4900 accept(new FormulaVo(reason.getSubstituteFormula()));
1123    }
1124  5119 setLocationWithinModule(context);
1125  5119 visitor.visitLeave(reason);
1126  5119 setLocationWithinModule(context);
1127    }
1128   
 
1129  82 toggle public void accept(final Existential reason) throws ModuleDataException {
1130  82 checkForInterrupt();
1131  81 if (blocked || reason == null) {
1132  1 return;
1133    }
1134  80 final String context = getCurrentContext().getLocationWithinModule();
1135  80 visitor.visitEnter(reason);
1136  77 if (reason.getSubjectVariable() != null) {
1137  51 setLocationWithinModule(context + ".getSubjectVariable()");
1138  51 accept(reason.getSubjectVariable());
1139    }
1140  77 setLocationWithinModule(context);
1141  77 visitor.visitLeave(reason);
1142  77 setLocationWithinModule(context);
1143    }
1144   
 
1145  313 toggle public void accept(final Universal reason) throws ModuleDataException {
1146  313 checkForInterrupt();
1147  312 if (blocked || reason == null) {
1148  1 return;
1149    }
1150  311 final String context = getCurrentContext().getLocationWithinModule();
1151  311 visitor.visitEnter(reason);
1152  298 if (reason.getSubjectVariable() != null) {
1153  222 setLocationWithinModule(context + ".getSubjectVariable()");
1154  222 accept(reason.getSubjectVariable());
1155    }
1156  298 setLocationWithinModule(context);
1157  298 visitor.visitLeave(reason);
1158  298 setLocationWithinModule(context);
1159    }
1160   
 
1161  14609 toggle public void accept(final ConditionalProof reason) throws ModuleDataException {
1162  14609 checkForInterrupt();
1163  14608 if (blocked || reason == null) {
1164  921 return;
1165    }
1166  13687 final String context = getCurrentContext().getLocationWithinModule();
1167  13687 visitor.visitEnter(reason);
1168  13587 if (reason.getHypothesis() != null) {
1169  13582 setLocationWithinModule(context + ".getHypothesis()");
1170  13582 accept(reason.getHypothesis());
1171    }
1172  13537 if (reason.getFormalProofLineList() != null) {
1173  13528 setLocationWithinModule(context + ".getFormalProofLineList()");
1174  13528 accept(reason.getFormalProofLineList());
1175    }
1176  9183 if (reason.getConclusion() != null) {
1177  9178 setLocationWithinModule(context + ".getConclusion()");
1178  9178 accept(reason.getConclusion());
1179    }
1180  7471 setLocationWithinModule(context);
1181  7471 visitor.visitLeave(reason);
1182  7471 setLocationWithinModule(context);
1183    }
1184   
 
1185  13584 toggle public void accept(final Hypothesis hypothesis) throws ModuleDataException {
1186  13584 checkForInterrupt();
1187  13583 if (blocked || hypothesis == null) {
1188  6213 return;
1189    }
1190  7370 final String context = getCurrentContext().getLocationWithinModule();
1191  7370 visitor.visitEnter(hypothesis);
1192  7320 if (hypothesis.getFormula() != null) {
1193  7319 setLocationWithinModule(context + ".getFormula()");
1194  7319 accept(hypothesis.getFormula());
1195    }
1196  7320 setLocationWithinModule(context);
1197  7320 visitor.visitLeave(hypothesis);
1198  7320 setLocationWithinModule(context);
1199    }
1200   
 
1201  9180 toggle public void accept(final Conclusion conclusion) throws ModuleDataException {
1202  9180 checkForInterrupt();
1203  9179 if (blocked || conclusion == null) {
1204  6213 return;
1205    }
1206  2966 final String context = getCurrentContext().getLocationWithinModule();
1207  2966 visitor.visitEnter(conclusion);
1208  2866 if (conclusion.getFormula() != null) {
1209  2865 setLocationWithinModule(context + ".getFormula()");
1210  2865 accept(conclusion.getFormula());
1211    }
1212  1254 setLocationWithinModule(context);
1213  1254 visitor.visitLeave(conclusion);
1214  1254 setLocationWithinModule(context);
1215    }
1216   
 
1217  317131 toggle public void accept(final Formula formula) throws ModuleDataException {
1218  317131 checkForInterrupt();
1219  317130 if (blocked || formula == null) {
1220  210162 return;
1221    }
1222  106968 final String context = getCurrentContext().getLocationWithinModule();
1223  106968 visitor.visitEnter(formula);
1224  104978 if (formula.getElement() != null) {
1225  104971 setLocationWithinModule(context + ".getElement()");
1226  104971 accept(formula.getElement());
1227    }
1228  56445 setLocationWithinModule(context);
1229  56445 visitor.visitLeave(formula);
1230  56445 setLocationWithinModule(context);
1231    }
1232   
 
1233  434 toggle public void accept(final Term term) throws ModuleDataException {
1234  434 checkForInterrupt();
1235  433 if (blocked || term == null) {
1236  1 return;
1237    }
1238  432 final String context = getCurrentContext().getLocationWithinModule();
1239  432 visitor.visitEnter(term);
1240  432 if (term.getElement() != null) {
1241  432 setLocationWithinModule(context + ".getElement()");
1242  432 accept(term.getElement());
1243    }
1244  432 setLocationWithinModule(context);
1245  432 visitor.visitLeave(term);
1246  432 setLocationWithinModule(context);
1247    }
1248   
 
1249  1122350 toggle public void accept(final Element element) throws ModuleDataException {
1250  1122350 checkForInterrupt();
1251  1122349 if (blocked || element == null) {
1252  326065 return;
1253    }
1254  796284 final String context = getCurrentContext().getLocationWithinModule();
1255  796284 if (element.isList()) {
1256  595535 setLocationWithinModule(context + ".getList()");
1257  595535 accept(element.getList());
1258  200749 } else if (element.isAtom()) {
1259  200749 setLocationWithinModule(context + ".getAtom()");
1260  200749 accept(element.getAtom());
1261    } else {
1262  0 throw new IllegalArgumentException("unexpected element type: "
1263    + element.toString());
1264    }
1265  630258 setLocationWithinModule(context);
1266    }
1267   
 
1268  200751 toggle public void accept(final Atom atom) throws ModuleDataException {
1269  200751 checkForInterrupt();
1270  200750 if (blocked || atom == null) {
1271  1 return;
1272    }
1273  200749 final String context = getCurrentContext().getLocationWithinModule();
1274  200749 visitor.visitEnter(atom);
1275  200749 setLocationWithinModule(context);
1276  200749 visitor.visitLeave(atom);
1277  200749 setLocationWithinModule(context);
1278    }
1279   
 
1280  595537 toggle public void accept(final ElementList list) throws ModuleDataException {
1281  595537 checkForInterrupt();
1282  595536 if (blocked || list == null) {
1283  1 return;
1284    }
1285  595535 final String context = getCurrentContext().getLocationWithinModule();
1286  595535 visitor.visitEnter(list);
1287  1438982 for (int i = 0; i < list.size(); i++) {
1288  1009473 setLocationWithinModule(context + ".getElement(" + i + ")");
1289  1009473 accept(list.getElement(i));
1290    }
1291  429509 setLocationWithinModule(context);
1292  429509 visitor.visitLeave(list);
1293  429509 setLocationWithinModule(context);
1294    }
1295   
 
1296  1487130 toggle public void accept(final LatexList latexList) throws ModuleDataException {
1297  1487130 checkForInterrupt();
1298  1487129 if (blocked || latexList == null) {
1299  1049733 return;
1300    }
1301  437396 final String context = getCurrentContext().getLocationWithinModule();
1302  437396 visitor.visitEnter(latexList);
1303  1218048 for (int i = 0; i < latexList.size(); i++) {
1304  787552 setLocationWithinModule(context + ".get(" + i + ")");
1305  787552 accept(latexList.get(i));
1306    }
1307  430496 setLocationWithinModule(context);
1308  430496 visitor.visitLeave(latexList);
1309  430496 setLocationWithinModule(context);
1310    }
1311   
 
1312  789122 toggle public void accept(final Latex latex) throws ModuleDataException {
1313  789122 checkForInterrupt();
1314  789121 if (blocked || latex == null) {
1315  579154 return;
1316    }
1317  209967 final String context = getCurrentContext().getLocationWithinModule();
1318  209967 visitor.visitEnter(latex);
1319  206440 setLocationWithinModule(context);
1320  206440 visitor.visitLeave(latex);
1321  206440 setLocationWithinModule(context);
1322    }
1323   
1324    /**
1325    * Get node that is currently parsed. Might be <code>null</code>.
1326    *
1327    * @return QEDEQ node were are currently in.
1328    */
 
1329  40211 toggle public Node getNode() {
1330  40211 return node;
1331    }
1332   
1333    /**
1334    * Set location information where are we within the original module.
1335    *
1336    * @param locationWithinModule Location within module.
1337    */
 
1338  14861500 toggle public void setLocationWithinModule(final String locationWithinModule) {
1339  14861500 getCurrentContext().setLocationWithinModule(locationWithinModule);
1340    }
1341   
 
1342  27478425 toggle public final ModuleContext getCurrentContext() {
1343  27478425 return currentContext;
1344    }
1345   
1346    /**
1347    * Is further traversing blocked?
1348    *
1349    * @return Is further traversing blocked?
1350    */
 
1351  394 toggle public final boolean getBlocked() {
1352  394 return blocked;
1353    }
1354   
1355    /**
1356    * Set if further traverse is blocked.
1357    *
1358    * @param blocked Further transversion?
1359    */
 
1360  2636423 toggle public final void setBlocked(final boolean blocked) {
1361  2636423 this.blocked = blocked;
1362    }
1363   
1364    /**
1365    * Get calculated visit percentage.
1366    *
1367    * @return Value between 0 and 100.
1368    */
 
1369  0 toggle public double getVisitPercentage() {
1370  0 if (data == null) {
1371  0 return 0;
1372    }
1373  0 return data.getVisitPercentage();
1374    }
1375   
1376    /**
1377    * Set absolute location description.
1378    *
1379    * @param text Description.
1380    */
 
1381  380825 toggle private void setLocation(final String text) {
1382  380825 location.setSize(0);
1383  380825 location.push(text);
1384    }
1385   
 
1386  17 toggle public String getLocationDescription() {
1387  17 final StringBuffer buffer = new StringBuffer();
1388  68 for (int i = 0; i < location.size(); i++) {
1389  51 if (i > 0) {
1390  34 buffer.append(" / ");
1391    }
1392  51 buffer.append(location.get(i));
1393    }
1394  17 return buffer.toString();
1395    }
1396   
1397    /**
1398    * Get copy of current counters.
1399    *
1400    * @return Values of various counters.
1401    */
 
1402  20354 toggle public QedeqNumbers getCurrentNumbers() {
1403  20354 return new QedeqNumbers(data);
1404    }
1405   
1406    /**
1407    * Get current (QEDEQ module local) rule version for given rule name.
1408    *
1409    * @param name Rule name
1410    * @return Current (local) rule version. Might be <code>null</code>.
1411    */
 
1412  3086 toggle public RuleKey getLocalRuleKey(final String name) {
1413  3086 return (RuleKey) ruleExistence.get(name);
1414    }
1415   
1416    }
1417   
 
CloverReport generated by Clover Code Coverage v3.1.10
Fri May 24 2013 13:47:32 UTC.		   Clover: Open Source License registered to qedeq.org .