|
1 |
| |
|
2 |
| |
|
3 |
| |
|
4 |
| |
|
5 |
| |
|
6 |
| |
|
7 |
| |
|
8 |
| |
|
9 |
| |
|
10 |
| |
|
11 |
| |
|
12 |
| |
|
13 |
| |
|
14 |
| |
|
15 |
| |
|
16 |
| |
|
17 |
| |
|
18 |
| package org.qedeq.kernel.xml.mapper; |
|
19 |
| |
|
20 |
| import java.util.ArrayList; |
|
21 |
| import java.util.HashMap; |
|
22 |
| import java.util.List; |
|
23 |
| import java.util.Map; |
|
24 |
| |
|
25 |
| import org.qedeq.kernel.base.list.ElementList; |
|
26 |
| import org.qedeq.kernel.base.module.Author; |
|
27 |
| import org.qedeq.kernel.base.module.AuthorList; |
|
28 |
| import org.qedeq.kernel.base.module.Axiom; |
|
29 |
| import org.qedeq.kernel.base.module.Chapter; |
|
30 |
| import org.qedeq.kernel.base.module.ChapterList; |
|
31 |
| import org.qedeq.kernel.base.module.Formula; |
|
32 |
| import org.qedeq.kernel.base.module.FunctionDefinition; |
|
33 |
| import org.qedeq.kernel.base.module.Header; |
|
34 |
| import org.qedeq.kernel.base.module.Import; |
|
35 |
| import org.qedeq.kernel.base.module.ImportList; |
|
36 |
| import org.qedeq.kernel.base.module.Latex; |
|
37 |
| import org.qedeq.kernel.base.module.LatexList; |
|
38 |
| import org.qedeq.kernel.base.module.LinkList; |
|
39 |
| import org.qedeq.kernel.base.module.LiteratureItem; |
|
40 |
| import org.qedeq.kernel.base.module.LiteratureItemList; |
|
41 |
| import org.qedeq.kernel.base.module.Location; |
|
42 |
| import org.qedeq.kernel.base.module.LocationList; |
|
43 |
| import org.qedeq.kernel.base.module.Node; |
|
44 |
| import org.qedeq.kernel.base.module.PredicateDefinition; |
|
45 |
| import org.qedeq.kernel.base.module.Proof; |
|
46 |
| import org.qedeq.kernel.base.module.ProofList; |
|
47 |
| import org.qedeq.kernel.base.module.Proposition; |
|
48 |
| import org.qedeq.kernel.base.module.Qedeq; |
|
49 |
| import org.qedeq.kernel.base.module.Rule; |
|
50 |
| import org.qedeq.kernel.base.module.Section; |
|
51 |
| import org.qedeq.kernel.base.module.SectionList; |
|
52 |
| import org.qedeq.kernel.base.module.Specification; |
|
53 |
| import org.qedeq.kernel.base.module.Subsection; |
|
54 |
| import org.qedeq.kernel.base.module.SubsectionList; |
|
55 |
| import org.qedeq.kernel.base.module.Term; |
|
56 |
| import org.qedeq.kernel.base.module.UsedByList; |
|
57 |
| import org.qedeq.kernel.base.module.VariableList; |
|
58 |
| import org.qedeq.kernel.bo.module.ModuleContext; |
|
59 |
| import org.qedeq.kernel.bo.module.ModuleDataException; |
|
60 |
| import org.qedeq.kernel.bo.visitor.AbstractModuleVisitor; |
|
61 |
| import org.qedeq.kernel.bo.visitor.QedeqNotNullTransverser; |
|
62 |
| import org.qedeq.kernel.dto.list.Enumerator; |
|
63 |
| import org.qedeq.kernel.trace.Trace; |
|
64 |
| import org.qedeq.kernel.xml.tracker.SimpleXPath; |
|
65 |
| |
|
66 |
| |
|
67 |
| |
|
68 |
| |
|
69 |
| |
|
70 |
| |
|
71 |
| |
|
72 |
| |
|
73 |
| |
|
74 |
| |
|
75 |
| |
|
76 |
| |
|
77 |
| |
|
78 |
| |
|
79 |
| |
|
80 |
| |
|
81 |
| |
|
82 |
| |
|
83 |
| |
|
84 |
| |
|
85 |
| |
|
86 |
| |
|
87 |
| public final class Context2SimpleXPath extends AbstractModuleVisitor { |
|
88 |
| |
|
89 |
| |
|
90 |
| private QedeqNotNullTransverser transverser; |
|
91 |
| |
|
92 |
| |
|
93 |
| private Qedeq qedeq; |
|
94 |
| |
|
95 |
| |
|
96 |
| private final ModuleContext find; |
|
97 |
| |
|
98 |
| |
|
99 |
| private SimpleXPath current; |
|
100 |
| |
|
101 |
| |
|
102 |
| private final List elements; |
|
103 |
| |
|
104 |
| |
|
105 |
| private int level; |
|
106 |
| |
|
107 |
| |
|
108 |
| private boolean matching; |
|
109 |
| |
|
110 |
| |
|
111 |
| private String matchingBegin; |
|
112 |
| |
|
113 |
| |
|
114 |
| private SimpleXPath matchingPath; |
|
115 |
| |
|
116 |
| |
|
117 |
| |
|
118 |
| |
|
119 |
| |
|
120 |
| |
|
121 |
| |
|
122 |
32947
| private Context2SimpleXPath(final ModuleContext find, final Qedeq qedeq) {
|
|
123 |
32947
| this.qedeq = qedeq;
|
|
124 |
32947
| transverser = new QedeqNotNullTransverser(find.getModuleLocation(), this);
|
|
125 |
32947
| this.find = find;
|
|
126 |
32947
| elements = new ArrayList(20);
|
|
127 |
| } |
|
128 |
| |
|
129 |
| |
|
130 |
| |
|
131 |
| |
|
132 |
| |
|
133 |
| |
|
134 |
| |
|
135 |
| |
|
136 |
| |
|
137 |
| |
|
138 |
| |
|
139 |
| |
|
140 |
| |
|
141 |
| |
|
142 |
| |
|
143 |
| |
|
144 |
| |
|
145 |
| |
|
146 |
| |
|
147 |
| |
|
148 |
| |
|
149 |
| |
|
150 |
| |
|
151 |
| |
|
152 |
| |
|
153 |
| |
|
154 |
32947
| public static SimpleXPath getXPath(final ModuleContext find, final Qedeq qedeq)
|
|
155 |
| throws ModuleDataException { |
|
156 |
32947
| final Context2SimpleXPath converter = new Context2SimpleXPath(find, qedeq);
|
|
157 |
32947
| return converter.find();
|
|
158 |
| } |
|
159 |
| |
|
160 |
32947
| private final SimpleXPath find() throws ModuleDataException {
|
|
161 |
32947
| final String method = "find()";
|
|
162 |
32947
| Trace.paramInfo(this, method, "find", find);
|
|
163 |
32947
| elements.clear();
|
|
164 |
32947
| level = 0;
|
|
165 |
32947
| current = new SimpleXPath();
|
|
166 |
32947
| try {
|
|
167 |
32947
| transverser.accept(qedeq);
|
|
168 |
| } catch (LocationFoundException e) { |
|
169 |
32947
| Trace.paramInfo(this, method, "location found", current);
|
|
170 |
32947
| return current;
|
|
171 |
| } |
|
172 |
0
| Trace.param(this, method, "level", level);
|
|
173 |
0
| Trace.info(this, method, "location was not found");
|
|
174 |
0
| throw new LocationNotFoundException(find);
|
|
175 |
| } |
|
176 |
| |
|
177 |
32947
| public final void visitEnter(final Qedeq qedeq) throws ModuleDataException {
|
|
178 |
32947
| enter("QEDEQ");
|
|
179 |
32947
| final String method = "visitEnter(Qedeq)";
|
|
180 |
32947
| Trace.param(this, method, "current", current);
|
|
181 |
32947
| checkMatching(method);
|
|
182 |
| } |
|
183 |
| |
|
184 |
0
| public final void visitLeave(final Qedeq qedeq) {
|
|
185 |
0
| leave();
|
|
186 |
| } |
|
187 |
| |
|
188 |
32945
| public final void visitEnter(final Header header) throws ModuleDataException {
|
|
189 |
32945
| enter("HEADER");
|
|
190 |
32945
| final String method = "visitEnter(Header)";
|
|
191 |
32945
| Trace.param(this, method, "current", current);
|
|
192 |
32945
| final String context = transverser.getCurrentContext().getLocationWithinModule();
|
|
193 |
32945
| checkMatching(method);
|
|
194 |
| |
|
195 |
32932
| transverser.setLocationWithinModule(context + ".getEmail()");
|
|
196 |
32932
| current.setAttribute("email");
|
|
197 |
32932
| checkIfFound();
|
|
198 |
| } |
|
199 |
| |
|
200 |
30137
| public final void visitLeave(final Header header) {
|
|
201 |
30137
| leave();
|
|
202 |
| } |
|
203 |
| |
|
204 |
2907
| public final void visitEnter(final Specification specification) throws ModuleDataException {
|
|
205 |
2907
| enter("SPECIFICATION");
|
|
206 |
2907
| final String method = "visitEnter(Specification)";
|
|
207 |
2907
| Trace.param(this, method, "current", current);
|
|
208 |
2907
| final String context = transverser.getCurrentContext().getLocationWithinModule();
|
|
209 |
2907
| checkMatching(method);
|
|
210 |
| |
|
211 |
2855
| transverser.setLocationWithinModule(context + ".getName()");
|
|
212 |
2855
| current.setAttribute("name");
|
|
213 |
2855
| checkIfFound();
|
|
214 |
| |
|
215 |
2831
| transverser.setLocationWithinModule(context + ".getRuleVersion()");
|
|
216 |
2831
| current.setAttribute("ruleVersion");
|
|
217 |
2831
| checkIfFound();
|
|
218 |
| } |
|
219 |
| |
|
220 |
2678
| public final void visitLeave(final Specification specification) {
|
|
221 |
2678
| leave();
|
|
222 |
| } |
|
223 |
| |
|
224 |
170319
| public final void visitEnter(final LatexList latexList) throws ModuleDataException {
|
|
225 |
170319
| final String method = "visitEnter(LatexList)";
|
|
226 |
170319
| final String context = transverser.getCurrentContext().getLocationWithinModule();
|
|
227 |
170319
| final String name;
|
|
228 |
170319
| if (context.endsWith(".getTitle()")) {
|
|
229 |
72519
| name = "TITLE";
|
|
230 |
97800
| } else if (context.endsWith(".getSummary()")) {
|
|
231 |
2632
| name = "ABSTRACT";
|
|
232 |
95168
| } else if (context.endsWith(".getIntroduction()")) {
|
|
233 |
58098
| name = "INTRODUCTION";
|
|
234 |
37070
| } else if (context.endsWith(".getName()")) {
|
|
235 |
11451
| name = "NAME";
|
|
236 |
25619
| } else if (context.endsWith(".getPrecedingText()")) {
|
|
237 |
24909
| name = "PRECEDING";
|
|
238 |
710
| } else if (context.endsWith(".getSucceedingText()")) {
|
|
239 |
276
| name = "SUCCEEDING";
|
|
240 |
434
| } else if (context.endsWith(".getLatex()")) {
|
|
241 |
150
| name = "TEXT";
|
|
242 |
284
| } else if (context.endsWith(".getDescription()")) {
|
|
243 |
120
| name = "DESCRIPTION";
|
|
244 |
164
| } else if (context.endsWith(".getNonFormalProof()")) {
|
|
245 |
66
| name = null;
|
|
246 |
98
| } else if (context.endsWith(".getItem()")) {
|
|
247 |
98
| name = null;
|
|
248 |
| } else { |
|
249 |
0
| throw new IllegalArgumentException("unknown LatexList " + context);
|
|
250 |
| } |
|
251 |
170319
| Trace.param(this, method, "name", name);
|
|
252 |
170319
| if (name != null) {
|
|
253 |
170155
| enter(name);
|
|
254 |
| } |
|
255 |
170319
| Trace.param(this, method, "current", current);
|
|
256 |
| |
|
257 |
170319
| checkMatching(method);
|
|
258 |
| } |
|
259 |
| |
|
260 |
165273
| public final void visitLeave(final LatexList latexList) {
|
|
261 |
165273
| final String context = transverser.getCurrentContext().getLocationWithinModule();
|
|
262 |
165273
| if (!context.endsWith(".getNonFormalProof()")
|
|
263 |
| && !context.endsWith(".getItem()")) { |
|
264 |
165273
| leave();
|
|
265 |
| } |
|
266 |
| } |
|
267 |
| |
|
268 |
3865
| public final void visitEnter(final Latex latex) throws ModuleDataException {
|
|
269 |
3865
| final String context = transverser.getCurrentContext().getLocationWithinModule();
|
|
270 |
3865
| if (context.indexOf(".getAuthorList().get(") >= 0) {
|
|
271 |
13
| enter("NAME");
|
|
272 |
| } |
|
273 |
3865
| enter("LATEX");
|
|
274 |
3865
| final String method = "visitEnter(Latex)";
|
|
275 |
3865
| Trace.param(this, method, "current", current);
|
|
276 |
3865
| checkMatching(method);
|
|
277 |
| |
|
278 |
1206
| transverser.setLocationWithinModule(context + ".getLanguage()");
|
|
279 |
1206
| current.setAttribute("language");
|
|
280 |
1206
| checkIfFound();
|
|
281 |
| |
|
282 |
1206
| transverser.setLocationWithinModule(context + ".getLatex()");
|
|
283 |
1206
| current.setAttribute(null);
|
|
284 |
1206
| checkIfFound();
|
|
285 |
| } |
|
286 |
| |
|
287 |
1206
| public final void visitLeave(final Latex latex) {
|
|
288 |
| |
|
289 |
1206
| final String context = transverser.getCurrentContext().getLocationWithinModule();
|
|
290 |
1206
| if (context.indexOf(".getAuthorList().get(") >= 0) {
|
|
291 |
0
| leave();
|
|
292 |
| } |
|
293 |
1206
| leave();
|
|
294 |
| } |
|
295 |
| |
|
296 |
129
| public final void visitEnter(final LocationList locationList) throws ModuleDataException {
|
|
297 |
129
| enter("LOCATIONS");
|
|
298 |
129
| final String method = "visitEnter(LocationList)";
|
|
299 |
129
| Trace.param(this, method, "current", current);
|
|
300 |
129
| checkMatching(method);
|
|
301 |
| |
|
302 |
| } |
|
303 |
| |
|
304 |
0
| public final void visitLeave(final LocationList locationList) {
|
|
305 |
0
| leave();
|
|
306 |
| } |
|
307 |
| |
|
308 |
77
| public final void visitEnter(final Location location) throws ModuleDataException {
|
|
309 |
77
| enter("LOCATION");
|
|
310 |
77
| final String method = "visitEnter(Location)";
|
|
311 |
77
| Trace.param(this, method, "current", current);
|
|
312 |
77
| final String context = transverser.getCurrentContext().getLocationWithinModule();
|
|
313 |
77
| checkMatching(method);
|
|
314 |
| |
|
315 |
24
| transverser.setLocationWithinModule(context + ".getLocation()");
|
|
316 |
24
| current.setAttribute("value");
|
|
317 |
24
| checkIfFound();
|
|
318 |
| } |
|
319 |
| |
|
320 |
0
| public final void visitLeave(final Location location) {
|
|
321 |
0
| leave();
|
|
322 |
| } |
|
323 |
| |
|
324 |
2586
| public final void visitEnter(final AuthorList authorList) throws ModuleDataException {
|
|
325 |
2586
| enter("AUTHORS");
|
|
326 |
2586
| final String method = "visitEnter(AuthorList)";
|
|
327 |
2586
| Trace.param(this, method, "current", current);
|
|
328 |
2586
| checkMatching(method);
|
|
329 |
| } |
|
330 |
| |
|
331 |
2514
| public final void visitLeave(final AuthorList authorList) {
|
|
332 |
2514
| leave();
|
|
333 |
| } |
|
334 |
| |
|
335 |
48
| public final void visitEnter(final Author author) throws ModuleDataException {
|
|
336 |
48
| enter("AUTHOR");
|
|
337 |
48
| final String method = "visitEnter(Author)";
|
|
338 |
48
| Trace.param(this, method, "current", current);
|
|
339 |
48
| final String context = transverser.getCurrentContext().getLocationWithinModule();
|
|
340 |
48
| checkMatching(method);
|
|
341 |
| |
|
342 |
24
| transverser.setLocationWithinModule(context + ".getEmail()");
|
|
343 |
24
| current.setAttribute("email");
|
|
344 |
24
| checkIfFound();
|
|
345 |
| } |
|
346 |
| |
|
347 |
0
| public final void visitLeave(final Author author) {
|
|
348 |
0
| leave();
|
|
349 |
| } |
|
350 |
| |
|
351 |
2492
| public final void visitEnter(final ImportList importList) throws ModuleDataException {
|
|
352 |
2492
| enter("IMPORTS");
|
|
353 |
2492
| final String method = "visitEnter(ImportList)";
|
|
354 |
2492
| Trace.param(this, method, "current", current);
|
|
355 |
2492
| checkMatching(method);
|
|
356 |
| } |
|
357 |
| |
|
358 |
33
| public final void visitLeave(final ImportList importList) {
|
|
359 |
33
| leave();
|
|
360 |
| } |
|
361 |
| |
|
362 |
3015
| public final void visitEnter(final Import imp) throws ModuleDataException {
|
|
363 |
3015
| enter("IMPORT");
|
|
364 |
3015
| final String method = "visitEnter(Import)";
|
|
365 |
3015
| Trace.param(this, method, "current", current);
|
|
366 |
3015
| final String context = transverser.getCurrentContext().getLocationWithinModule();
|
|
367 |
3015
| checkMatching(method);
|
|
368 |
| |
|
369 |
654
| transverser.setLocationWithinModule(context + ".getLabel()");
|
|
370 |
654
| current.setAttribute("label");
|
|
371 |
654
| checkIfFound();
|
|
372 |
| } |
|
373 |
| |
|
374 |
568
| public final void visitLeave(final Import imp) {
|
|
375 |
568
| leave();
|
|
376 |
| } |
|
377 |
| |
|
378 |
55
| public final void visitEnter(final UsedByList usedByList) throws ModuleDataException {
|
|
379 |
55
| enter("USEDBY");
|
|
380 |
55
| final String method = "visitEnter(UsedByList)";
|
|
381 |
55
| Trace.param(this, method, "current", current);
|
|
382 |
55
| checkMatching(method);
|
|
383 |
| } |
|
384 |
| |
|
385 |
0
| public final void visitLeave(final UsedByList usedByList) {
|
|
386 |
0
| leave();
|
|
387 |
| } |
|
388 |
| |
|
389 |
30137
| public final void visitEnter(final ChapterList chapterList) throws ModuleDataException {
|
|
390 |
30137
| final String method = "visitEnter(ChapterList)";
|
|
391 |
| |
|
392 |
| |
|
393 |
30137
| checkMatching(method);
|
|
394 |
| } |
|
395 |
| |
|
396 |
170
| public final void visitLeave(final ChapterList chapterList) {
|
|
397 |
170
| transverser.setBlocked(false);
|
|
398 |
| } |
|
399 |
| |
|
400 |
129385
| public final void visitEnter(final Chapter chapter) throws ModuleDataException {
|
|
401 |
129385
| enter("CHAPTER");
|
|
402 |
129385
| final String method = "visitEnter(Chapter)";
|
|
403 |
129385
| Trace.param(this, method, "current", current);
|
|
404 |
129385
| final String context = transverser.getCurrentContext().getLocationWithinModule();
|
|
405 |
129385
| checkMatching(method);
|
|
406 |
| |
|
407 |
129260
| transverser.setLocationWithinModule(context + ".getNoNumber()");
|
|
408 |
129260
| current.setAttribute("noNumber");
|
|
409 |
129260
| checkIfFound();
|
|
410 |
| } |
|
411 |
| |
|
412 |
99430
| public final void visitLeave(final Chapter chapter) {
|
|
413 |
99430
| leave();
|
|
414 |
| } |
|
415 |
| |
|
416 |
29331
| public final void visitEnter(final SectionList sectionList) throws ModuleDataException {
|
|
417 |
29331
| final String method = "visitEnter(SectionList)";
|
|
418 |
| |
|
419 |
| |
|
420 |
29331
| checkMatching(method);
|
|
421 |
| } |
|
422 |
| |
|
423 |
0
| public final void visitLeave(final SectionList sectionList) {
|
|
424 |
0
| transverser.setBlocked(false);
|
|
425 |
| } |
|
426 |
| |
|
427 |
72556
| public final void visitEnter(final Section section) throws ModuleDataException {
|
|
428 |
72556
| enter("SECTION");
|
|
429 |
72556
| final String method = "visitEnter(Section)";
|
|
430 |
72556
| Trace.param(this, method, "current", current);
|
|
431 |
72556
| final String context = transverser.getCurrentContext().getLocationWithinModule();
|
|
432 |
72556
| checkMatching(method);
|
|
433 |
| |
|
434 |
72323
| transverser.setLocationWithinModule(context + ".getNoNumber()");
|
|
435 |
72323
| current.setAttribute("noNumber");
|
|
436 |
72323
| checkIfFound();
|
|
437 |
| } |
|
438 |
| |
|
439 |
43300
| public final void visitLeave(final Section section) {
|
|
440 |
43300
| leave();
|
|
441 |
| } |
|
442 |
| |
|
443 |
28109
| public final void visitEnter(final SubsectionList subsectionList) throws ModuleDataException {
|
|
444 |
28109
| enter("SUBSECTIONS");
|
|
445 |
28109
| final String method = "visitEnter(SubsectionList)";
|
|
446 |
28109
| Trace.param(this, method, "current", current);
|
|
447 |
28109
| checkMatching(method);
|
|
448 |
| } |
|
449 |
| |
|
450 |
0
| public final void visitLeave(final SubsectionList subsectionList) {
|
|
451 |
0
| leave();
|
|
452 |
| } |
|
453 |
| |
|
454 |
3354
| public final void visitEnter(final Subsection subsection) throws ModuleDataException {
|
|
455 |
3354
| enter("SUBSECTION");
|
|
456 |
3354
| final String method = "visitEnter(Subsection)";
|
|
457 |
3354
| Trace.param(this, method, "current", current);
|
|
458 |
3354
| final String context = transverser.getCurrentContext().getLocationWithinModule();
|
|
459 |
3354
| checkMatching(method);
|
|
460 |
| |
|
461 |
3260
| transverser.setLocationWithinModule(context + ".getId()");
|
|
462 |
3260
| current.setAttribute("id");
|
|
463 |
3260
| checkIfFound();
|
|
464 |
| |
|
465 |
3260
| transverser.setLocationWithinModule(context + ".getLevel()");
|
|
466 |
3260
| current.setAttribute("level");
|
|
467 |
3260
| checkIfFound();
|
|
468 |
| } |
|
469 |
| |
|
470 |
2990
| public final void visitLeave(final Subsection subsection) {
|
|
471 |
2990
| leave();
|
|
472 |
| } |
|
473 |
| |
|
474 |
136469
| public final void visitEnter(final Node node) throws ModuleDataException {
|
|
475 |
136469
| enter("NODE");
|
|
476 |
136469
| final String method = "visitEnter(Node)";
|
|
477 |
136469
| Trace.param(this, method, "current", current);
|
|
478 |
136469
| final String context = transverser.getCurrentContext().getLocationWithinModule();
|
|
479 |
136469
| checkMatching(method);
|
|
480 |
| |
|
481 |
135830
| transverser.setLocationWithinModule(context + ".getId()");
|
|
482 |
135830
| current.setAttribute("id");
|
|
483 |
135830
| checkIfFound();
|
|
484 |
| |
|
485 |
135603
| transverser.setLocationWithinModule(context + ".getLevel()");
|
|
486 |
135603
| current.setAttribute("level");
|
|
487 |
135603
| checkIfFound();
|
|
488 |
| |
|
489 |
| |
|
490 |
135459
| transverser.setLocationWithinModule(context + ".getNodeType()");
|
|
491 |
135459
| current.setAttribute(null);
|
|
492 |
135459
| checkIfFound();
|
|
493 |
| |
|
494 |
| } |
|
495 |
| |
|
496 |
108841
| public final void visitLeave(final Node node) {
|
|
497 |
108841
| leave();
|
|
498 |
| } |
|
499 |
| |
|
500 |
2153
| public final void visitEnter(final Axiom axiom) throws ModuleDataException {
|
|
501 |
2153
| enter("AXIOM");
|
|
502 |
2153
| final String method = "visitEnter(Axiom)";
|
|
503 |
2153
| Trace.param(this, method, "current", current);
|
|
504 |
2153
| checkMatching(method);
|
|
505 |
| } |
|
506 |
| |
|
507 |
68
| public final void visitLeave(final Axiom axiom) {
|
|
508 |
68
| leave();
|
|
509 |
| } |
|
510 |
| |
|
511 |
17878
| public final void visitEnter(final Proposition proposition) throws ModuleDataException {
|
|
512 |
17878
| enter("THEOREM");
|
|
513 |
17878
| final String method = "visitEnter(Proposition)";
|
|
514 |
17878
| Trace.param(this, method, "current", current);
|
|
515 |
17878
| checkMatching(method);
|
|
516 |
| } |
|
517 |
| |
|
518 |
56
| public final void visitLeave(final Proposition proposition) {
|
|
519 |
56
| leave();
|
|
520 |
| } |
|
521 |
| |
|
522 |
152
| public final void visitEnter(final ProofList proofList) throws ModuleDataException {
|
|
523 |
152
| final String method = "visitEnter(ProofList)";
|
|
524 |
| |
|
525 |
| |
|
526 |
152
| checkMatching(method);
|
|
527 |
| } |
|
528 |
| |
|
529 |
124
| public final void visitEnter(final Proof proof) throws ModuleDataException {
|
|
530 |
124
| enter("PROOF");
|
|
531 |
124
| final String method = "visitEnter(Proof)";
|
|
532 |
124
| Trace.param(this, method, "current", current);
|
|
533 |
124
| final String context = transverser.getCurrentContext().getLocationWithinModule();
|
|
534 |
124
| checkMatching(method);
|
|
535 |
| |
|
536 |
86
| transverser.setLocationWithinModule(context + ".getKind()");
|
|
537 |
86
| current.setAttribute("kind");
|
|
538 |
86
| checkIfFound();
|
|
539 |
| |
|
540 |
76
| transverser.setLocationWithinModule(context + ".getLevel()");
|
|
541 |
76
| current.setAttribute("level");
|
|
542 |
76
| checkIfFound();
|
|
543 |
| } |
|
544 |
| |
|
545 |
0
| public final void visitLeave(final Proof proof) {
|
|
546 |
0
| leave();
|
|
547 |
| } |
|
548 |
| |
|
549 |
1376
| public final void visitEnter(final PredicateDefinition definition) throws ModuleDataException {
|
|
550 |
1376
| enter("DEFINITION_PREDICATE");
|
|
551 |
1376
| final String method = "visitEnter(PredicateDefinition)";
|
|
552 |
1376
| Trace.param(this, method, "current", current);
|
|
553 |
1376
| final String context = transverser.getCurrentContext().getLocationWithinModule();
|
|
554 |
1376
| checkMatching(method);
|
|
555 |
| |
|
556 |
1302
| transverser.setLocationWithinModule(context + ".getArgumentNumber()");
|
|
557 |
1302
| current.setAttribute("arguments");
|
|
558 |
1302
| checkIfFound();
|
|
559 |
| |
|
560 |
1272
| transverser.setLocationWithinModule(context + ".getName()");
|
|
561 |
1272
| current.setAttribute("name");
|
|
562 |
1272
| checkIfFound();
|
|
563 |
| |
|
564 |
1242
| transverser.setLocationWithinModule(context + ".getLatexPattern()");
|
|
565 |
1242
| enter("LATEXPATTERN");
|
|
566 |
1242
| if (find.getLocationWithinModule().equals(transverser.getCurrentContext()
|
|
567 |
| .getLocationWithinModule())) { |
|
568 |
30
| if (definition.getLatexPattern() == null) {
|
|
569 |
0
| leave();
|
|
570 |
| } |
|
571 |
30
| throw new LocationFoundException(transverser.getCurrentContext());
|
|
572 |
| } |
|
573 |
1212
| leave();
|
|
574 |
| } |
|
575 |
| |
|
576 |
80
| public final void visitLeave(final PredicateDefinition definition) {
|
|
577 |
80
| leave();
|
|
578 |
| } |
|
579 |
| |
|
580 |
2062
| public final void visitEnter(final FunctionDefinition definition) throws ModuleDataException {
|
|
581 |
2062
| enter("DEFINITION_FUNCTION");
|
|
582 |
2062
| final String method = "visitEnter(FunctionDefinition)";
|
|
583 |
2062
| Trace.param(this, method, "current", current);
|
|
584 |
2062
| final String context = transverser.getCurrentContext().getLocationWithinModule();
|
|
585 |
2062
| checkMatching(method);
|
|
586 |
| |
|
587 |
1966
| transverser.setLocationWithinModule(context + ".getArgumentNumber()");
|
|
588 |
1966
| current.setAttribute("arguments");
|
|
589 |
1966
| checkIfFound();
|
|
590 |
| |
|
591 |
1934
| transverser.setLocationWithinModule(context + ".getName()");
|
|
592 |
1934
| current.setAttribute("name");
|
|
593 |
1934
| checkIfFound();
|
|
594 |
| |
|
595 |
1902
| transverser.setLocationWithinModule(context + ".getLatexPattern()");
|
|
596 |
1902
| enter("LATEXPATTERN");
|
|
597 |
1902
| if (find.getLocationWithinModule().equals(transverser.getCurrentContext()
|
|
598 |
| .getLocationWithinModule())) { |
|
599 |
32
| if (definition.getLatexPattern() == null) {
|
|
600 |
0
| leave();
|
|
601 |
| } |
|
602 |
32
| throw new LocationFoundException(transverser.getCurrentContext());
|
|
603 |
| } |
|
604 |
1870
| leave();
|
|
605 |
| } |
|
606 |
| |
|
607 |
42
| public final void visitLeave(final FunctionDefinition definition) {
|
|
608 |
42
| leave();
|
|
609 |
| } |
|
610 |
| |
|
611 |
162
| public final void visitEnter(final Rule rule) throws ModuleDataException {
|
|
612 |
162
| enter("RULE");
|
|
613 |
162
| final String method = "visitEnter(Rule)";
|
|
614 |
162
| Trace.param(this, method, "current", current);
|
|
615 |
162
| final String context = transverser.getCurrentContext().getLocationWithinModule();
|
|
616 |
162
| checkMatching(method);
|
|
617 |
| |
|
618 |
128
| transverser.setLocationWithinModule(context + ".getName()");
|
|
619 |
128
| current.setAttribute("name");
|
|
620 |
128
| checkIfFound();
|
|
621 |
| } |
|
622 |
| |
|
623 |
30
| public final void visitLeave(final Rule rule) {
|
|
624 |
30
| leave();
|
|
625 |
| } |
|
626 |
| |
|
627 |
22
| public final void visitEnter(final LinkList linkList) throws ModuleDataException {
|
|
628 |
22
| final String method = "visitEnter(LinkList)";
|
|
629 |
22
| Trace.param(this, method, "current", current);
|
|
630 |
22
| final String context = transverser.getCurrentContext().getLocationWithinModule();
|
|
631 |
22
| checkMatching(method);
|
|
632 |
| |
|
633 |
16
| for (int i = 0; i < linkList.size(); i++) {
|
|
634 |
16
| enter("LINK");
|
|
635 |
16
| if (linkList.get(i) != null) {
|
|
636 |
16
| transverser.setLocationWithinModule(context + ".get(" + i + ")");
|
|
637 |
16
| current.setAttribute("id");
|
|
638 |
16
| checkIfFound();
|
|
639 |
| } |
|
640 |
14
| leave();
|
|
641 |
| }; |
|
642 |
| } |
|
643 |
| |
|
644 |
14
| public final void visitLeave(final LinkList linkList) {
|
|
645 |
| } |
|
646 |
| |
|
647 |
20397
| public final void visitEnter(final Formula formula) throws ModuleDataException {
|
|
648 |
20397
| enter("FORMULA");
|
|
649 |
20397
| final String method = "visitEnter(Formula)";
|
|
650 |
20397
| Trace.param(this, method, "current", current);
|
|
651 |
20397
| checkMatching(method);
|
|
652 |
| } |
|
653 |
| |
|
654 |
220
| public final void visitLeave(final Formula formula) {
|
|
655 |
220
| leave();
|
|
656 |
| } |
|
657 |
| |
|
658 |
1576
| public final void visitEnter(final Term term) throws ModuleDataException {
|
|
659 |
1576
| enter("TERM");
|
|
660 |
1576
| final String method = "visitEnter(Term)";
|
|
661 |
1576
| Trace.param(this, method, "current", current);
|
|
662 |
1576
| checkMatching(method);
|
|
663 |
| } |
|
664 |
| |
|
665 |
42
| public final void visitLeave(final Term term) {
|
|
666 |
42
| leave();
|
|
667 |
| } |
|
668 |
| |
|
669 |
2834
| public final void visitEnter(final VariableList variableList) throws ModuleDataException {
|
|
670 |
2834
| enter("VARLIST");
|
|
671 |
2834
| final String method = "visitEnter(VariableList)";
|
|
672 |
2834
| Trace.param(this, method, "current", current);
|
|
673 |
2834
| checkMatching(method);
|
|
674 |
| } |
|
675 |
| |
|
676 |
2270
| public final void visitLeave(final VariableList variableList) {
|
|
677 |
2270
| leave();
|
|
678 |
| } |
|
679 |
| |
|
680 |
182020
| public final void visitEnter(final ElementList list) throws ModuleDataException {
|
|
681 |
182020
| final String operator = list.getOperator();
|
|
682 |
182020
| enter(operator);
|
|
683 |
182020
| final String method = "visitEnter(ElementList)";
|
|
684 |
182020
| Trace.param(this, method, "current", current);
|
|
685 |
182020
| final String context = transverser.getCurrentContext().getLocationWithinModule();
|
|
686 |
| |
|
687 |
| |
|
688 |
182020
| if (context.startsWith(find.getLocationWithinModule())) {
|
|
689 |
19133
| throw new LocationFoundException(find);
|
|
690 |
| } |
|
691 |
| |
|
692 |
162887
| checkMatching(method);
|
|
693 |
| |
|
694 |
162887
| transverser.setLocationWithinModule(context + ".getOperator()");
|
|
695 |
162887
| checkIfFound();
|
|
696 |
162887
| transverser.setLocationWithinModule(context);
|
|
697 |
162887
| final boolean firstIsAtom = list.size() > 0 && list.getElement(0).isAtom();
|
|
698 |
162887
| if (firstIsAtom) {
|
|
699 |
58662
| transverser.setLocationWithinModule(context + ".getElement(0).getAtom()");
|
|
700 |
58662
| if ("VAR".equals(operator) || "PREDVAR".equals(operator)
|
|
701 |
| || "FUNVAR".equals(operator)) { |
|
702 |
13635
| current.setAttribute("id");
|
|
703 |
13635
| checkIfFound();
|
|
704 |
45027
| } else if ("PREDCON".equals(operator) || "FUNCON".equals(operator)) {
|
|
705 |
45027
| current.setAttribute("ref");
|
|
706 |
45027
| checkIfFound();
|
|
707 |
| } else { |
|
708 |
0
| current.setAttribute(null);
|
|
709 |
0
| Trace.info(this, method, "unknown operator " + operator);
|
|
710 |
0
| throw new LocationFoundException(transverser.getCurrentContext());
|
|
711 |
| } |
|
712 |
| } |
|
713 |
| } |
|
714 |
| |
|
715 |
| |
|
716 |
| |
|
717 |
| |
|
718 |
| |
|
719 |
| |
|
720 |
| |
|
721 |
| |
|
722 |
| |
|
723 |
| |
|
724 |
102867
| public final void visitLeave(final ElementList list) {
|
|
725 |
102867
| leave();
|
|
726 |
| } |
|
727 |
| |
|
728 |
170
| public final void visitEnter(final LiteratureItemList list) throws ModuleDataException {
|
|
729 |
170
| enter("BIBLIOGRAPHY");
|
|
730 |
170
| final String method = "visitEnter(LiteratureItemList)";
|
|
731 |
170
| Trace.param(this, method, "current", current);
|
|
732 |
170
| checkMatching(method);
|
|
733 |
| } |
|
734 |
| |
|
735 |
0
| public final void visitLeave(final LiteratureItemList list) {
|
|
736 |
0
| leave();
|
|
737 |
| } |
|
738 |
| |
|
739 |
524
| public final void visitEnter(final LiteratureItem item) throws ModuleDataException {
|
|
740 |
524
| enter("ITEM");
|
|
741 |
524
| final String method = "visitEnter(LiteratureItem)";
|
|
742 |
524
| Trace.param(this, method, "current", current);
|
|
743 |
524
| final String context = transverser.getCurrentContext().getLocationWithinModule();
|
|
744 |
524
| checkMatching(method);
|
|
745 |
| |
|
746 |
478
| transverser.setLocationWithinModule(context + ".getLabel()");
|
|
747 |
478
| current.setAttribute("label");
|
|
748 |
478
| checkIfFound();
|
|
749 |
| } |
|
750 |
| |
|
751 |
360
| public final void visitLeave(final LiteratureItem item) {
|
|
752 |
360
| leave();
|
|
753 |
| } |
|
754 |
| |
|
755 |
| |
|
756 |
| |
|
757 |
| |
|
758 |
| |
|
759 |
| |
|
760 |
1778577
| private final void checkIfFound() throws LocationFoundException {
|
|
761 |
1778577
| if (find.getLocationWithinModule().equals(transverser.getCurrentContext()
|
|
762 |
| .getLocationWithinModule())) { |
|
763 |
13752
| throw new LocationFoundException(transverser.getCurrentContext());
|
|
764 |
| } |
|
765 |
| } |
|
766 |
| |
|
767 |
| |
|
768 |
| |
|
769 |
| |
|
770 |
| |
|
771 |
| |
|
772 |
| |
|
773 |
| |
|
774 |
| |
|
775 |
| |
|
776 |
| |
|
777 |
| |
|
778 |
893043
| private final void checkMatching(final String method)
|
|
779 |
| throws LocationNotFoundException, LocationFoundException { |
|
780 |
893043
| final String context = transverser.getCurrentContext().getLocationWithinModule();
|
|
781 |
893043
| if (find.getLocationWithinModule().startsWith(context)) {
|
|
782 |
329854
| Trace.info(this, method, "beginning matches");
|
|
783 |
329854
| Trace.paramInfo(this, method, "context", context);
|
|
784 |
329854
| matching = true;
|
|
785 |
329854
| matchingBegin = context;
|
|
786 |
329854
| matchingPath = new SimpleXPath(current);
|
|
787 |
| } else { |
|
788 |
563189
| if (matching) {
|
|
789 |
| |
|
790 |
| |
|
791 |
| |
|
792 |
| |
|
793 |
| |
|
794 |
| |
|
795 |
563189
| if (!context.startsWith(matchingBegin)) {
|
|
796 |
| |
|
797 |
| |
|
798 |
| |
|
799 |
| |
|
800 |
0
| Trace.info(this, method, "matching lost");
|
|
801 |
0
| Trace.paramInfo(this, method, "last match ", matchingBegin);
|
|
802 |
0
| Trace.paramInfo(this, method, "current context", context);
|
|
803 |
0
| Trace.paramInfo(this, method, "find context ",
|
|
804 |
| find.getLocationWithinModule()); |
|
805 |
| |
|
806 |
| |
|
807 |
| |
|
808 |
0
| Trace.traceStack(this, method);
|
|
809 |
0
| Trace.info(this, method, "changing XPath to last matching one");
|
|
810 |
| |
|
811 |
| |
|
812 |
| |
|
813 |
0
| current = matchingPath;
|
|
814 |
0
| throw new LocationFoundException(new ModuleContext(find.getModuleLocation(),
|
|
815 |
| matchingBegin)); |
|
816 |
| } |
|
817 |
| } |
|
818 |
563189
| transverser.setBlocked(true);
|
|
819 |
| } |
|
820 |
893043
| checkIfFound();
|
|
821 |
| } |
|
822 |
| |
|
823 |
| |
|
824 |
| |
|
825 |
| |
|
826 |
| |
|
827 |
| |
|
828 |
855543
| private final void enter(final String element) {
|
|
829 |
855543
| level++;
|
|
830 |
855543
| current.addElement(element, addOccurence(element));
|
|
831 |
| } |
|
832 |
| |
|
833 |
| |
|
834 |
| |
|
835 |
| |
|
836 |
| |
|
837 |
| |
|
838 |
0
| private final void enterFirst(final String element) {
|
|
839 |
0
| level++;
|
|
840 |
0
| current.addElement(element);
|
|
841 |
| } |
|
842 |
| |
|
843 |
| |
|
844 |
| |
|
845 |
| |
|
846 |
566101
| private final void leave() {
|
|
847 |
566101
| level--;
|
|
848 |
566101
| current.deleteLastElement();
|
|
849 |
566101
| transverser.setBlocked(false);
|
|
850 |
| } |
|
851 |
| |
|
852 |
| |
|
853 |
| |
|
854 |
| |
|
855 |
| |
|
856 |
| |
|
857 |
| |
|
858 |
| |
|
859 |
| |
|
860 |
| |
|
861 |
| |
|
862 |
855543
| private final int addOccurence(final String name) {
|
|
863 |
855543
| while (level < elements.size()) {
|
|
864 |
122
| elements.remove(elements.size() - 1);
|
|
865 |
| } |
|
866 |
855543
| while (level > elements.size()) {
|
|
867 |
289679
| elements.add(new HashMap());
|
|
868 |
| } |
|
869 |
855543
| final Map levelMap = (Map) elements.get(level - 1);
|
|
870 |
855543
| final Enumerator counter;
|
|
871 |
855543
| if (levelMap.containsKey(name)) {
|
|
872 |
330501
| counter = (Enumerator) levelMap.get(name);
|
|
873 |
330501
| counter.increaseNumber();
|
|
874 |
| } else { |
|
875 |
525042
| counter = new Enumerator(1);
|
|
876 |
525042
| levelMap.put(name, counter);
|
|
877 |
| } |
|
878 |
855543
| return counter.getNumber();
|
|
879 |
| } |
|
880 |
| |
|
881 |
| } |