|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
ControlVisitor | Line # 46 | 155 | 85 | 78.2% |
0.7818182
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||
(66) | |||
Result | |||
0.58181816
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegativeGeneration2 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegativeGeneration2 | 1 PASS | |
0.58181816
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testGeneration2 org.qedeq.kernel.bo.latex.GenerateLatexTest.testGeneration2 | 1 PASS | |
0.58181816
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegativeGeneration2 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegativeGeneration2 | 1 PASS | |
0.58181816
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testGeneration org.qedeq.kernel.bo.latex.GenerateLatexTest.testGeneration | 1 PASS | |
0.58181816
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testGeneration2 org.qedeq.kernel.bo.latex.GenerateLatexTest.testGeneration2 | 1 PASS | |
0.44727272
|
org.qedeq.kernel.bo.service.latex.Qedeq2LatexTest.testQ2L003 org.qedeq.kernel.bo.service.latex.Qedeq2LatexTest.testQ2L003 | 1 PASS | |
0.43636364
|
org.qedeq.kernel.bo.service.logic.FormalProofCheckerPluginTest.testPlugin3 org.qedeq.kernel.bo.service.logic.FormalProofCheckerPluginTest.testPlugin3 | 1 PASS | |
0.36
|
org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration1 org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration1 | 1 PASS | |
0.23272727
|
org.qedeq.kernel.bo.service.logic.SimpleProofFinderPluginTest.testPlugin org.qedeq.kernel.bo.service.logic.SimpleProofFinderPluginTest.testPlugin | 1 PASS | |
0.23272727
|
org.qedeq.kernel.bo.service.logic.SimpleProofFinderPluginTest.testPlugin2 org.qedeq.kernel.bo.service.logic.SimpleProofFinderPluginTest.testPlugin2 | 1 PASS | |
0.23272727
|
org.qedeq.kernel.bo.service.logic.SimpleProofFinderPluginTest.testPluginFast org.qedeq.kernel.bo.service.logic.SimpleProofFinderPluginTest.testPluginFast | 1 PASS | |
0.21818182
|
org.qedeq.kernel.bo.service.logic.FormalProofCheckerPluginTest.testPlugin2 org.qedeq.kernel.bo.service.logic.FormalProofCheckerPluginTest.testPlugin2 | 1 PASS | |
0.18181819
|
org.qedeq.kernel.bo.service.latex.Qedeq2LatexTest.testQ2L001_v2 org.qedeq.kernel.bo.service.latex.Qedeq2LatexTest.testQ2L001_v2 | 1 PASS | |
0.18181819
|
org.qedeq.kernel.bo.service.latex.Qedeq2LatexTest.testQ2L001_v1 org.qedeq.kernel.bo.service.latex.Qedeq2LatexTest.testQ2L001_v1 | 1 PASS | |
0.17818181
|
org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration2 org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration2 | 1 PASS | |
0.17090909
|
org.qedeq.kernel.bo.service.heuristic.HeuristicCheckerPluginTest.testQedeqSetTheoryScript1 org.qedeq.kernel.bo.service.heuristic.HeuristicCheckerPluginTest.testQedeqSetTheoryScript1 | 1 PASS | |
0.17090909
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_02 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_02 | 1 PASS | |
0.17090909
|
org.qedeq.kernel.bo.service.heuristic.HeuristicCheckerPluginTest.testQedeqSetTheoryScript2 org.qedeq.kernel.bo.service.heuristic.HeuristicCheckerPluginTest.testQedeqSetTheoryScript2 | 1 PASS | |
0.17090909
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_03 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_03 | 1 PASS | |
0.17090909
|
org.qedeq.kernel.bo.service.latex.Qedeq2LatexTest.testQ2L002 org.qedeq.kernel.bo.service.latex.Qedeq2LatexTest.testQ2L002 | 1 PASS | |
0.16727273
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative08 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative08 | 1 PASS | |
0.16727273
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_09 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_09 | 1 PASS | |
0.16727273
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative08 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative08 | 1 PASS | |
0.16363636
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative06 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative06 | 1 PASS | |
0.16363636
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative05 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative05 | 1 PASS | |
0.16363636
|
org.qedeq.kernel.bo.service.logic.QedeqBoFormalLogicCheckerTest.testCheckModule org.qedeq.kernel.bo.service.logic.QedeqBoFormalLogicCheckerTest.testCheckModule | 1 PASS | |
0.16363636
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative06 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative06 | 1 PASS | |
0.16363636
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative05 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative05 | 1 PASS | |
0.16363636
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_08 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_08 | 1 PASS | |
0.16363636
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative07 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative07 | 1 PASS | |
0.16363636
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative07 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative07 | 1 PASS | |
0.15636364
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_10 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_10 | 1 PASS | |
0.15636364
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_11 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_11 | 1 PASS | |
0.15636364
|
org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testNegative04 org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testNegative04 | 1 PASS | |
0.15636364
|
org.qedeq.kernel.xml.parser.CharsetParserTest.testParse1 org.qedeq.kernel.xml.parser.CharsetParserTest.testParse1 | 1 PASS | |
0.15636364
|
org.qedeq.kernel.xml.parser.CharsetParserTest.testParse2 org.qedeq.kernel.xml.parser.CharsetParserTest.testParse2 | 1 PASS | |
0.15272728
|
org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration6 org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration6 | 1 PASS | |
0.15272728
|
org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration5 org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration5 | 1 PASS | |
0.14909092
|
org.qedeq.kernel.bo.service.logic.QedeqBoFormalLogicCheckerDirectTest.testNegative04 org.qedeq.kernel.bo.service.logic.QedeqBoFormalLogicCheckerDirectTest.testNegative04 | 1 PASS | |
0.14909092
|
org.qedeq.kernel.bo.service.logic.QedeqBoFormalLogicCheckerDirectTest.testNegative02 org.qedeq.kernel.bo.service.logic.QedeqBoFormalLogicCheckerDirectTest.testNegative02 | 1 PASS | |
0.14909092
|
org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testNegative02 org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testNegative02 | 1 PASS | |
0.14909092
|
org.qedeq.kernel.bo.service.logic.QedeqBoFormalLogicCheckerDirectTest.testNegative03 org.qedeq.kernel.bo.service.logic.QedeqBoFormalLogicCheckerDirectTest.testNegative03 | 1 PASS | |
0.14909092
|
org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testNegative03 org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testNegative03 | 1 PASS | |
0.14181818
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_12 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_12 | 1 PASS | |
0.14181818
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_07 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_07 | 1 PASS | |
0.13454546
|
org.qedeq.kernel.bo.service.control.QedeqBoFactoryTest.testCreateStringQedeq5 org.qedeq.kernel.bo.service.control.QedeqBoFactoryTest.testCreateStringQedeq5 | 1 PASS | |
0.13454546
|
org.qedeq.kernel.bo.service.control.QedeqBoFactoryTest.testCreateStringQedeq4 org.qedeq.kernel.bo.service.control.QedeqBoFactoryTest.testCreateStringQedeq4 | 1 PASS | |
0.12727273
|
org.qedeq.kernel.bo.logic.proof.checker.ProofCheckerTest.testCheck6 org.qedeq.kernel.bo.logic.proof.checker.ProofCheckerTest.testCheck6 | 1 PASS | |
0.12727273
|
org.qedeq.kernel.bo.logic.proof.finder.ProofFinderImplTest.testFind org.qedeq.kernel.bo.logic.proof.finder.ProofFinderImplTest.testFind | 1 PASS | |
0.12727273
|
org.qedeq.kernel.bo.service.control.LoadRequiredModulesTest.testLoadRequiredModules_10 org.qedeq.kernel.bo.service.control.LoadRequiredModulesTest.testLoadRequiredModules_10 | 1 PASS | |
0.12727273
|
org.qedeq.kernel.bo.logic.proof.finder.ProofFinderImplTest.testFind2 org.qedeq.kernel.bo.logic.proof.finder.ProofFinderImplTest.testFind2 | 1 PASS | |
0.12727273
|
org.qedeq.kernel.bo.logic.proof.checker.ProofCheckerTest.testCheck4 org.qedeq.kernel.bo.logic.proof.checker.ProofCheckerTest.testCheck4 | 1 PASS | |
0.12727273
|
org.qedeq.kernel.bo.logic.proof.checker.ProofCheckerTest.testCheck1 org.qedeq.kernel.bo.logic.proof.checker.ProofCheckerTest.testCheck1 | 1 PASS | |
0.12727273
|
org.qedeq.kernel.bo.logic.proof.finder.ProofFinderImplTest.testFind3 org.qedeq.kernel.bo.logic.proof.finder.ProofFinderImplTest.testFind3 | 1 PASS | |
0.12727273
|
org.qedeq.kernel.bo.service.control.QedeqBoFactoryTest.testCreateStringQedeq6 org.qedeq.kernel.bo.service.control.QedeqBoFactoryTest.testCreateStringQedeq6 | 1 PASS | |
0.11272727
|
org.qedeq.kernel.xml.dao.GenerateXmlTest.testGeneration org.qedeq.kernel.xml.dao.GenerateXmlTest.testGeneration | 1 PASS | |
0.10909091
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative02 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative02 | 1 PASS | |
0.10909091
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative02 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative02 | 1 PASS | |
0.10909091
|
org.qedeq.kernel.bo.service.control.QedeqBoFactoryTest.testCreateStringQedeq1 org.qedeq.kernel.bo.service.control.QedeqBoFactoryTest.testCreateStringQedeq1 | 1 PASS | |
0.10545454
|
org.qedeq.kernel.bo.service.control.LoadRequiredModulesTest.testLoadRequiredModules_03 org.qedeq.kernel.bo.service.control.LoadRequiredModulesTest.testLoadRequiredModules_03 | 1 PASS | |
0.10545454
|
org.qedeq.kernel.bo.service.control.LoadRequiredModulesTest.testLoadRequiredModules_04 org.qedeq.kernel.bo.service.control.LoadRequiredModulesTest.testLoadRequiredModules_04 | 1 PASS | |
0.10545454
|
org.qedeq.kernel.bo.service.control.LoadRequiredModulesTest.testLoadRequiredModules_02 org.qedeq.kernel.bo.service.control.LoadRequiredModulesTest.testLoadRequiredModules_02 | 1 PASS | |
0.10545454
|
org.qedeq.kernel.bo.service.control.LoadRequiredModulesTest.testLoadRequiredModules_09 org.qedeq.kernel.bo.service.control.LoadRequiredModulesTest.testLoadRequiredModules_09 | 1 PASS | |
0.10545454
|
org.qedeq.kernel.bo.service.control.LoadRequiredModulesTest.testLoadRequiredModules_07 org.qedeq.kernel.bo.service.control.LoadRequiredModulesTest.testLoadRequiredModules_07 | 1 PASS | |
0.10181818
|
org.qedeq.kernel.bo.service.control.QedeqBoFactoryTest.testCreateStringQedeq3 org.qedeq.kernel.bo.service.control.QedeqBoFactoryTest.testCreateStringQedeq3 | 1 PASS | |
0.10181818
|
org.qedeq.kernel.bo.service.control.QedeqBoFactoryTest.testCreateStringQedeq2 org.qedeq.kernel.bo.service.control.QedeqBoFactoryTest.testCreateStringQedeq2 | 1 PASS | |
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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | public Service getService() { |
281 | 380 | return service; |
282 | } | |
283 | ||
284 | /** | |
285 | * Get location info from traverser. | |
286 | * | |
287 | * @return Location description. | |
288 | */ | |
289 | 17 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | public QedeqTraverser getTraverser() { |
576 | 0 | return traverser; |
577 | } | |
578 | ||
579 | } |
|