Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
../../../../../img/srcFileCovDistChart8.png 62% of files have more coverage
155   579   85   5.54
92   340   0.55   28
28     3.04  
1    
 
  ControlVisitor       Line # 46 155 85 78.2% 0.7818182
 
  (66)
 
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.bo.module;
17   
18    import org.qedeq.base.io.SourceArea;
19    import org.qedeq.base.trace.Trace;
20    import org.qedeq.base.utility.StringUtility;
21    import org.qedeq.kernel.se.base.module.Axiom;
22    import org.qedeq.kernel.se.base.module.FunctionDefinition;
23    import org.qedeq.kernel.se.base.module.Node;
24    import org.qedeq.kernel.se.base.module.PredicateDefinition;
25    import org.qedeq.kernel.se.base.module.Proposition;
26    import org.qedeq.kernel.se.base.module.Rule;
27    import org.qedeq.kernel.se.common.ModuleContext;
28    import org.qedeq.kernel.se.common.ModuleDataException;
29    import org.qedeq.kernel.se.common.RuleKey;
30    import org.qedeq.kernel.se.common.Service;
31    import org.qedeq.kernel.se.common.SourceFileException;
32    import org.qedeq.kernel.se.common.SourceFileExceptionList;
33    import org.qedeq.kernel.se.visitor.AbstractModuleVisitor;
34    import org.qedeq.kernel.se.visitor.InterruptException;
35    import org.qedeq.kernel.se.visitor.QedeqNotNullTraverser;
36    import org.qedeq.kernel.se.visitor.QedeqNumbers;
37    import org.qedeq.kernel.se.visitor.QedeqTraverser;
38   
39   
40    /**
41    * Basic visitor that gives some error collecting features. Also hides the
42    * traverser that does the work.
43    *
44    * @author Michael Meyling
45    */
 
46    public abstract class ControlVisitor extends AbstractModuleVisitor {
47   
48    /** This class. */
49    private static final Class CLASS = ControlVisitor.class;
50   
51    /** This service we work for. */
52    private final Service service;
53   
54    /** QEDEQ BO object to work on. */
55    private final KernelQedeqBo prop;
56   
57    /** We work in this service call. */
58    private InternalServiceCall call;
59   
60    /** Traverse QEDEQ module with this traverser. */
61    private final QedeqNotNullTraverser traverser;
62   
63    /** List of Exceptions of type error during Module visit. */
64    private SourceFileExceptionList errorList;
65   
66    /** List of Exceptions of type warnings during Module visit. */
67    private SourceFileExceptionList warningList;
68   
69    /** Was traverse interrupted by user? */
70    private boolean interrupted;
71   
72    /**
73    * Constructor. Can only be used if instance also implements {@link Service}.
74    *
75    * @param prop Internal QedeqBo.
76    */
 
77  0 toggle protected ControlVisitor(final KernelQedeqBo prop) {
78  0 this.prop = prop;
79  0 this.service = (Service) this;
80  0 this.traverser = new QedeqNotNullTraverser(prop.getModuleAddress(), this);
81  0 this.errorList = new SourceFileExceptionList();
82  0 this.warningList = new SourceFileExceptionList();
83    }
84   
85    /**
86    * Constructor.
87    *
88    * @param service This service we work for.
89    * @param prop Internal QedeqBo.
90    */
 
91  2177 toggle protected ControlVisitor(final Service service, final KernelQedeqBo prop) {
92  2177 this.service = service;
93  2177 this.prop = prop;
94  2177 this.traverser = new QedeqNotNullTraverser(prop.getModuleAddress(), this);
95  2177 this.errorList = new SourceFileExceptionList();
96  2177 this.warningList = new SourceFileExceptionList();
97    }
98   
99    /**
100    * Get QedeqBo.
101    *
102    * @return QEDEQ module were are in.
103    */
 
104  215956 toggle public KernelQedeqBo getQedeqBo() {
105  215956 return this.prop;
106    }
107   
108    /**
109    * Get node that is currently parsed. Might be <code>null</code>.
110    *
111    * @return QEDEQ node were are currently in.
112    */
 
113  40211 toggle public KernelNodeBo getNodeBo() {
114  40211 final Node node = traverser.getNode();
115  40211 if (node == null || getQedeqBo() == null) {
116  59 return null;
117    }
118  40152 return getQedeqBo().getLabels().getNode(node.getId());
119    }
120   
121    /**
122    * Start traverse of QedeqBo. If during the traverse a {@link ModuleDataException}
123    * occurs it is thrown till high level, transformed into a
124    * {@link SourceFileException} and added to the error list. All collected exceptions
125    * (via {@link #addError(ModuleDataException)} and
126    * {@link #addError(SourceFileException)}) are thrown (if there were any).
127    * <br/>
128    * If you are interested in warnings you have to call {@link #getWarningList()} afterwards.
129    *
130    * @param process We work in this service process.
131    * @throws SourceFileExceptionList All collected error exceptions.
132    */
 
133  1547 toggle public void traverse(final InternalServiceProcess process) throws SourceFileExceptionList {
134  1547 this.call = process.getInternalServiceCall();
135  1547 interrupted = false;
136  1547 if (getQedeqBo().getQedeq() == null) {
137  0 addWarning(new SourceFileException(getService(),
138    ModuleErrors.QEDEQ_MODULE_NOT_LOADED_CODE,
139    ModuleErrors.QEDEQ_MODULE_NOT_LOADED_TEXT,
140    new IllegalArgumentException(),
141    new SourceArea(getQedeqBo().getModuleAddress().getUrl()),
142    null));
143  0 return; // we can do nothing without a loaded module
144    }
145  1547 try {
146  1547 this.traverser.accept(getQedeqBo().getQedeq());
147    } catch (InterruptException ie) {
148  0 addError(ie);
149  0 interrupted = true;
150    } catch (ModuleDataException me) {
151  8 addError(me);
152    } catch (RuntimeException e) {
153  0 Trace.fatal(CLASS, this, "traverse", "looks like a programming error", e);
154  0 addError(new RuntimeVisitorException(getCurrentContext(), e));
155    }
156  1547 if (errorList.size() > 0) {
157  36 throw errorList;
158    }
159    }
160   
161    /**
162    * Get current context within original. Remember to use the copy constructor
163    * when trying to remember this context!
164    *
165    * @return Current context.
166    */
 
167  250921 toggle public ModuleContext getCurrentContext() {
168  250921 return this.traverser.getCurrentContext();
169    }
170   
171    /**
172    * Add exception to error collection.
173    *
174    * @param me Exception to be added.
175    */
 
176  122 toggle protected void addError(final ModuleDataException me) {
177  122 addError(prop.createSourceFileException(getService(), me));
178    }
179   
180    /**
181    * Add exception to error collection.
182    *
183    * @param sf Exception to be added.
184    */
 
185  122 toggle protected void addError(final SourceFileException sf) {
186  122 errorList.add(sf);
187    }
188   
189    /**
190    * Get list of errors that occurred during visit.
191    *
192    * @return Exception list.
193    */
 
194  78 toggle public SourceFileExceptionList getErrorList() {
195  78 return errorList;
196    }
197   
198    /**
199    * Did any errors occur yet?
200    *
201    * @return Non error free visits?
202    */
 
203  0 toggle public boolean hasErrors() {
204  0 return errorList.size() > 0;
205    }
206   
207    /**
208    * Did no errors occur yet?
209    *
210    * @return Error free visits?
211    */
 
212  0 toggle public boolean hasNoErrors() {
213  0 return !hasErrors();
214    }
215   
216    /**
217    * Add exception to warning collection.
218    *
219    * @param me Exception to be added.
220    */
 
221  114 toggle protected void addWarning(final ModuleDataException me) {
222    // TODO 20101026 m31: here no SourcefileException should be added!
223    // there might exist different representations (e.g. XML, utf8 text, html)
224    // and we might want to resolve the location for them also.
225    // And perhaps resolving all error locations at the same time is
226    // faster because one has to load the source file only once...
227  114 addWarning(prop.createSourceFileException(getService(), me));
228    }
229   
230    /**
231    * Add exception to warning collection.
232    *
233    * @param sf Exception to be added.
234    */
 
235  114 toggle private void addWarning(final SourceFileException sf) {
236  114 warningList.add(sf);
237    }
238   
239    /**
240    * Get list of warnings that occurred during visit.
241    *
242    * @return Exception list.
243    */
 
244  71 toggle public SourceFileExceptionList getWarningList() {
245  71 return warningList;
246    }
247   
248    /**
249    * Set if further traverse is blocked.
250    *
251    * @param blocked Further traverse blocked?
252    */
 
253  75276 toggle protected void setBlocked(final boolean blocked) {
254  75276 traverser.setBlocked(blocked);
255    }
256   
257    /**
258    * Get if further traverse is blocked.
259    *
260    * @return Further traverse blocked?
261    */
 
262  394 toggle public boolean getBlocked() {
263  394 return traverser.getBlocked();
264    }
265   
266    /**
267    * Get service call we work in.
268    *
269    * @return Service process we work for.
270    */
 
271  229 toggle public InternalServiceCall getInternalServiceCall() {
272  229 return call;
273    }
274   
275    /**
276    * Get service we work for.
277    *
278    * @return Service we work for.
279    */
 
280  380 toggle public Service getService() {
281  380 return service;
282    }
283   
284    /**
285    * Get location info from traverser.
286    *
287    * @return Location description.
288    */
 
289  17 toggle public String getLocationDescription() {
290  17 return traverser.getLocationDescription();
291    }
292   
293    /**
294    * Get percentage of visit currently done.
295    *
296    * @return Value between 0 and 100.
297    */
 
298  0 toggle public double getVisitPercentage() {
299  0 return traverser.getVisitPercentage();
300    }
301   
302    /**
303    * Get copy of current counters.
304    *
305    * @return Values of various counters.
306    */
 
307  20354 toggle public QedeqNumbers getCurrentNumbers() {
308  20354 return traverser.getCurrentNumbers();
309    }
310   
311    /**
312    * Get current (QEDEQ module local) rule version for given rule name.
313    *
314    * @param name Rule name
315    * @return Current (local) rule version. Might be <code>null</code>.
316    */
 
317  3086 toggle public RuleKey getLocalRuleKey(final String name) {
318  3086 return traverser.getLocalRuleKey(name);
319    }
320   
321    /**
322    * Get internal kernel services. Convenience method.
323    *
324    * @return Internal kernel services.
325    */
 
326  72812 toggle public InternalKernelServices getServices() {
327  72812 return prop.getKernelServices();
328    }
329   
330    /**
331    * Was traverse interrupted by user?
332    *
333    * @return Did we get an interrupt?
334    */
 
335  850 toggle public boolean getInterrupted() {
336  850 return interrupted;
337    }
338   
339    /**
340    * Get link for given reference.
341    *
342    * @param reference String to parse.
343    * @param context Here the link is in the source text.
344    * @param addWarning Should we add a warning if an error occurs?
345    * @param addError Should we add an error if an error occurs?
346    * @return Generated link. Never <code>null</code>.
347    */
 
348  4818 toggle public Reference getReference(final String reference, final ModuleContext context,
349    final boolean addWarning, final boolean addError) {
350    // get node we are currently in
351  4818 KernelNodeBo node = getNodeBo();
352  4818 final Reference fallback = new DefaultReference(node, null, "", null,
353  4818 (reference != null ? reference : "") + "?", "", "");
354  4818 if (reference == null || reference.length() <= 0) {
355  4 return fallback;
356    }
357  4814 if (reference.indexOf("!") >= 0 && reference.indexOf("/") >= 0) {
358  0 if (addWarning) {
359  0 addWarning(new ReferenceLinkException(
360    ModuleErrors.REFERENCE_CAN_NOT_CONTAIN_SUB_AND_LINE_REFERENCE_CODE,
361    ModuleErrors.REFERENCE_CAN_NOT_CONTAIN_SUB_AND_LINE_REFERENCE_TEXT
362    + "\"" + reference + "\"", context));
363    }
364  0 if (addError) {
365  0 addError(new ReferenceLinkException(
366    ModuleErrors.REFERENCE_CAN_NOT_CONTAIN_SUB_AND_LINE_REFERENCE_CODE,
367    ModuleErrors.REFERENCE_CAN_NOT_CONTAIN_SUB_AND_LINE_REFERENCE_TEXT
368    + "\"" + reference + "\"", context));
369    }
370    }
371    // is the reference a pure proof line label?
372  4814 if (node != null && node.isProofLineLabel(reference)) {
373  2970 return new DefaultReference(node, null, "", node, node.getNodeVo().getId(), "", reference);
374    }
375    // is the reference a pure node label?
376  1844 if (getQedeqBo().getLabels().isNode(reference)) {
377  1530 return new DefaultReference(node, null, "", getQedeqBo().getLabels().getNode(
378    reference), reference, "", "");
379    }
380    // do we have an external module reference without node?
381  314 if (getQedeqBo().getLabels().isModule(reference)) {
382  10 return new DefaultReference(node,
383    (KernelQedeqBo) getQedeqBo().getLabels().getReferences().getQedeqBo(reference),
384    reference, null, "", "", "");
385   
386    }
387   
388  304 String moduleLabel = ""; // module import
389  304 String nodeLabel = ""; // module intern node reference
390  304 String lineLabel = ""; // proof line label
391  304 String subLabel = ""; // sub label
392   
393  304 final String[] split = StringUtility.split(reference, ".");
394  304 if (split.length <= 1 || split.length > 2) {
395  94 if (split.length == 1) {
396  82 nodeLabel = split[0];
397  12 } else if (split.length > 2) {
398  12 if (addWarning) {
399  12 addWarning(new ReferenceLinkException(
400    ModuleErrors.NODE_REFERENCE_HAS_MORE_THAN_ONE_DOT_CODE,
401    ModuleErrors.NODE_REFERENCE_HAS_MORE_THAN_ONE_DOT_TEXT
402    + "\"" + reference + "\"", context));
403    }
404  12 if (addError) {
405  0 addError(new ReferenceLinkException(
406    ModuleErrors.NODE_REFERENCE_HAS_MORE_THAN_ONE_DOT_CODE,
407    ModuleErrors.NODE_REFERENCE_HAS_MORE_THAN_ONE_DOT_TEXT
408    + "\"" + reference + "\"", context));
409    }
410  12 return fallback;
411    }
412    } else {
413  210 moduleLabel = split[0];
414  210 nodeLabel = split[1];
415    }
416   
417  292 if (nodeLabel.indexOf("!") >= 0) {
418  7 final String[] split2 = StringUtility.split(nodeLabel, "!");
419  7 if (split2.length != 2) {
420  0 if (addWarning) {
421  0 addWarning(new ReferenceLinkException(
422    ModuleErrors.NODE_REFERENCE_MUST_HAVE_ONLY_ONE_PROOF_LINE_REFERENCE_CODE,
423    ModuleErrors.NODE_REFERENCE_MUST_HAVE_ONLY_ONE_PROOF_LINE_REFERENCE_TEXT
424    + "\"" + reference + "\"", context));
425    }
426  0 if (addError) {
427  0 addError(new ReferenceLinkException(
428    ModuleErrors.NODE_REFERENCE_MUST_HAVE_ONLY_ONE_PROOF_LINE_REFERENCE_CODE,
429    ModuleErrors.NODE_REFERENCE_MUST_HAVE_ONLY_ONE_PROOF_LINE_REFERENCE_TEXT
430    + "\"" + reference + "\"", context));
431    }
432    }
433  7 nodeLabel = split2[0];
434  7 if (split.length > 1) {
435  0 lineLabel = split2[1];
436    }
437    }
438  292 if (nodeLabel.indexOf("/") >= 0) {
439  169 final String[] split2 = StringUtility.split(nodeLabel, "/");
440  169 if (split2.length != 2) {
441  0 if (addWarning) {
442  0 addWarning(new ReferenceLinkException(
443    ModuleErrors.NODE_REFERENCE_MUST_HAVE_ONLY_ONE_SUB_REFERENCE_CODE,
444    ModuleErrors.NODE_REFERENCE_MUST_HAVE_ONLY_ONE_SUB_REFERENCE_TEXT
445    + "\"" + reference + "\"", context));
446    }
447  0 if (addError) {
448  0 addError(new ReferenceLinkException(
449    ModuleErrors.NODE_REFERENCE_MUST_HAVE_ONLY_ONE_SUB_REFERENCE_CODE,
450    ModuleErrors.NODE_REFERENCE_MUST_HAVE_ONLY_ONE_SUB_REFERENCE_TEXT
451    + "\"" + reference + "\"", context));
452    }
453    }
454  169 nodeLabel = split2[0];
455  169 if (split.length > 1) {
456  114 subLabel = split2[1];
457    }
458    }
459  292 KernelQedeqBo module = null;
460  292 KernelNodeBo eNode = null;
461  292 if (moduleLabel != null && moduleLabel.length() > 0) {
462  210 module = getQedeqBo().getKernelRequiredModules().getKernelQedeqBo(moduleLabel);
463  210 eNode = (module != null ? module.getLabels().getNode(nodeLabel) : null);
464    } else {
465  82 eNode = getQedeqBo().getLabels().getNode(nodeLabel);
466    }
467  292 if ((moduleLabel != null && moduleLabel.length() > 0) && module == null) {
468  5 if (addWarning) {
469  4 addWarning(new ReferenceLinkException(
470    ModuleErrors.MODULE_REFERENCE_NOT_FOUND_CODE,
471    ModuleErrors.MODULE_REFERENCE_NOT_FOUND_TEXT
472    + "\"" + reference + "\"", context));
473    }
474  5 if (addError) {
475  0 addError(new ReferenceLinkException(
476    ModuleErrors.MODULE_REFERENCE_NOT_FOUND_CODE,
477    ModuleErrors.MODULE_REFERENCE_NOT_FOUND_TEXT
478    + "\"" + reference + "\"", context));
479    }
480  5 return new DefaultReference(node, module, moduleLabel + "?", eNode, nodeLabel, subLabel, lineLabel);
481    }
482  287 if (eNode == null) {
483  20 if (addWarning) {
484  18 addWarning(new ReferenceLinkException(
485    ModuleErrors.NODE_REFERENCE_NOT_FOUND_CODE,
486    ModuleErrors.NODE_REFERENCE_NOT_FOUND_TEXT
487    + "\"" + reference + "\"", context));
488    }
489  20 if (addError) {
490  0 addError(new ReferenceLinkException(
491    ModuleErrors.NODE_REFERENCE_NOT_FOUND_CODE,
492    ModuleErrors.NODE_REFERENCE_NOT_FOUND_TEXT
493    + "\"" + reference + "\"", context));
494    }
495  20 return new DefaultReference(node, module, moduleLabel, eNode, nodeLabel + "?", subLabel, lineLabel);
496    }
497  267 return new DefaultReference(node, module, moduleLabel, eNode, nodeLabel, subLabel, lineLabel);
498    }
499   
500    /**
501    * Get display text for node. The module of the node is ignored.
502    *
503    * @param label Label for node. Fallback if <code>kNode == null</code>.
504    * @param kNode Node for which we want a textual representation.
505    * @param language Language. Might be <code>null</code>.
506    * @return Textual node representation.
507    */
 
508  1363 toggle public String getNodeDisplay(final String label, final KernelNodeBo kNode, final String language) {
509  1363 String display = label;
510  1363 if (kNode == null) {
511  38 return display;
512    }
513  1325 QedeqNumbers data = kNode.getNumbers();
514  1325 Node node = kNode.getNodeVo();
515  1325 if (node.getNodeType() instanceof Axiom) {
516  654 if ("de".equals(language)) {
517  299 display = "Axiom";
518    } else {
519  355 display = "axiom";
520    }
521  654 display += " " + data.getAxiomNumber();
522  671 } else if (node.getNodeType() instanceof Proposition) {
523  427 if ("de".equals(language)) {
524  209 display = "Proposition";
525    } else {
526  218 display = "proposition";
527    }
528  427 display += " " + data.getPropositionNumber();
529  244 } else if (node.getNodeType() instanceof FunctionDefinition) {
530  60 if ("de".equals(language)) {
531  30 display = "Definition";
532    } else {
533  30 display = "definition";
534    }
535  60 display += " " + (data.getPredicateDefinitionNumber() + data.getFunctionDefinitionNumber());
536  184 } else if (node.getNodeType() instanceof PredicateDefinition) {
537  30 if ("de".equals(language)) {
538  15 display = "Definition";
539    } else {
540  15 display = "definition";
541    }
542  30 display += " " + (data.getPredicateDefinitionNumber() + data.getFunctionDefinitionNumber());
543  154 } else if (node.getNodeType() instanceof Rule) {
544  153 if ("de".equals(language)) {
545  78 display = "Regel";
546    } else {
547  75 display = "rule";
548    }
549  153 display += " " + data.getRuleNumber();
550    } else {
551  1 if ("de".equals(language)) {
552  0 display = "Unbekannt " + node.getId();
553    } else {
554  1 display = "unknown " + node.getId();
555    }
556    }
557  1325 return display;
558    }
559   
560    /**
561    * Set location information where are we within the original module.
562    *
563    * @param locationWithinModule Location within module.
564    */
 
565  71838 toggle public void setLocationWithinModule(final String locationWithinModule) {
566  71838 getCurrentContext().setLocationWithinModule(locationWithinModule);
567  71838 getServices().getContextChecker().checkContext(getQedeqBo().getQedeq(), getCurrentContext());
568    }
569   
570    /**
571    * Get traverser for QEDEQ module.
572    *
573    * @return Traverser used.
574    */
 
575  0 toggle public QedeqTraverser getTraverser() {
576  0 return traverser;
577    }
578   
579    }