|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||
QedeqVisitor | Line # 77 | 0 | 0 | - |
-1.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
No Tests | |||
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 org.qedeq.kernel.se.base.module.Add; | |
19 | import org.qedeq.kernel.se.base.module.Author; | |
20 | import org.qedeq.kernel.se.base.module.AuthorList; | |
21 | import org.qedeq.kernel.se.base.module.Axiom; | |
22 | import org.qedeq.kernel.se.base.module.ChangedRule; | |
23 | import org.qedeq.kernel.se.base.module.ChangedRuleList; | |
24 | import org.qedeq.kernel.se.base.module.Chapter; | |
25 | import org.qedeq.kernel.se.base.module.ChapterList; | |
26 | import org.qedeq.kernel.se.base.module.Conclusion; | |
27 | import org.qedeq.kernel.se.base.module.ConditionalProof; | |
28 | import org.qedeq.kernel.se.base.module.Existential; | |
29 | import org.qedeq.kernel.se.base.module.FormalProof; | |
30 | import org.qedeq.kernel.se.base.module.FormalProofLine; | |
31 | import org.qedeq.kernel.se.base.module.FormalProofLineList; | |
32 | import org.qedeq.kernel.se.base.module.FormalProofList; | |
33 | import org.qedeq.kernel.se.base.module.Formula; | |
34 | import org.qedeq.kernel.se.base.module.FunctionDefinition; | |
35 | import org.qedeq.kernel.se.base.module.Header; | |
36 | import org.qedeq.kernel.se.base.module.Hypothesis; | |
37 | import org.qedeq.kernel.se.base.module.Import; | |
38 | import org.qedeq.kernel.se.base.module.ImportList; | |
39 | import org.qedeq.kernel.se.base.module.InitialFunctionDefinition; | |
40 | import org.qedeq.kernel.se.base.module.InitialPredicateDefinition; | |
41 | import org.qedeq.kernel.se.base.module.Latex; | |
42 | import org.qedeq.kernel.se.base.module.LatexList; | |
43 | import org.qedeq.kernel.se.base.module.LinkList; | |
44 | import org.qedeq.kernel.se.base.module.LiteratureItem; | |
45 | import org.qedeq.kernel.se.base.module.LiteratureItemList; | |
46 | import org.qedeq.kernel.se.base.module.Location; | |
47 | import org.qedeq.kernel.se.base.module.LocationList; | |
48 | import org.qedeq.kernel.se.base.module.ModusPonens; | |
49 | import org.qedeq.kernel.se.base.module.Node; | |
50 | import org.qedeq.kernel.se.base.module.PredicateDefinition; | |
51 | import org.qedeq.kernel.se.base.module.Proof; | |
52 | import org.qedeq.kernel.se.base.module.ProofList; | |
53 | import org.qedeq.kernel.se.base.module.Proposition; | |
54 | import org.qedeq.kernel.se.base.module.Qedeq; | |
55 | import org.qedeq.kernel.se.base.module.Reason; | |
56 | import org.qedeq.kernel.se.base.module.Rename; | |
57 | import org.qedeq.kernel.se.base.module.Rule; | |
58 | import org.qedeq.kernel.se.base.module.Section; | |
59 | import org.qedeq.kernel.se.base.module.SectionList; | |
60 | import org.qedeq.kernel.se.base.module.Specification; | |
61 | import org.qedeq.kernel.se.base.module.Subsection; | |
62 | import org.qedeq.kernel.se.base.module.SubsectionList; | |
63 | import org.qedeq.kernel.se.base.module.SubsectionType; | |
64 | import org.qedeq.kernel.se.base.module.SubstFree; | |
65 | import org.qedeq.kernel.se.base.module.SubstFunc; | |
66 | import org.qedeq.kernel.se.base.module.SubstPred; | |
67 | import org.qedeq.kernel.se.base.module.Term; | |
68 | import org.qedeq.kernel.se.base.module.Universal; | |
69 | import org.qedeq.kernel.se.base.module.UsedByList; | |
70 | import org.qedeq.kernel.se.common.ModuleDataException; | |
71 | ||
72 | /** | |
73 | * Here are all elements to visit assembled that can be visited within a QEDEQ module. | |
74 | * | |
75 | * @author Michael Meyling | |
76 | */ | |
77 | public interface QedeqVisitor extends ListVisitor { | |
78 | ||
79 | /** | |
80 | * Visit certain element. Begin of visit. | |
81 | * | |
82 | * @param author Begin visit of this element. | |
83 | * @throws ModuleDataException Major problem occurred. | |
84 | */ | |
85 | public void visitEnter(Author author) throws ModuleDataException; | |
86 | ||
87 | /** | |
88 | * Visit certain element. Begin of visit. | |
89 | * | |
90 | * @param authorList Begin visit of this element. | |
91 | * @throws ModuleDataException Major problem occurred. | |
92 | */ | |
93 | public void visitEnter(AuthorList authorList) throws ModuleDataException; | |
94 | ||
95 | /** | |
96 | * Visit certain element. Begin of visit. | |
97 | * | |
98 | * @param axiom Begin visit of this element. | |
99 | * @throws ModuleDataException Major problem occurred. | |
100 | */ | |
101 | public void visitEnter(Axiom axiom) throws ModuleDataException; | |
102 | ||
103 | /** | |
104 | * Visit certain element. Begin of visit. | |
105 | * | |
106 | * @param chapter Begin visit of this element. | |
107 | * @throws ModuleDataException Major problem occurred. | |
108 | */ | |
109 | public void visitEnter(Chapter chapter) throws ModuleDataException; | |
110 | ||
111 | /** | |
112 | * Visit certain element. Begin of visit. | |
113 | * | |
114 | * @param chapterList Begin visit of this element. | |
115 | * @throws ModuleDataException Major problem occurred. | |
116 | */ | |
117 | public void visitEnter(ChapterList chapterList) throws ModuleDataException; | |
118 | ||
119 | /** | |
120 | * Visit certain element. Begin of visit. | |
121 | * | |
122 | * @param formula Begin visit of this element. | |
123 | * @throws ModuleDataException Major problem occurred. | |
124 | */ | |
125 | public void visitEnter(Formula formula) throws ModuleDataException; | |
126 | ||
127 | /** | |
128 | * Visit certain element. Begin of visit. | |
129 | * | |
130 | * @param functionDefinition Begin visit of this element. | |
131 | * @throws ModuleDataException Major problem occurred. | |
132 | */ | |
133 | public void visitEnter(InitialFunctionDefinition functionDefinition) throws ModuleDataException; | |
134 | ||
135 | /** | |
136 | * Visit certain element. Begin of visit. | |
137 | * | |
138 | * @param functionDefinition Begin visit of this element. | |
139 | * @throws ModuleDataException Major problem occurred. | |
140 | */ | |
141 | public void visitEnter(FunctionDefinition functionDefinition) throws ModuleDataException; | |
142 | ||
143 | /** | |
144 | * Visit certain element. Begin of visit. | |
145 | * | |
146 | * @param header Begin visit of this element. | |
147 | * @throws ModuleDataException Major problem occurred. | |
148 | */ | |
149 | public void visitEnter(Header header) throws ModuleDataException; | |
150 | ||
151 | /** | |
152 | * Visit certain element. Begin of visit. | |
153 | * | |
154 | * @param imp Begin visit of this element. | |
155 | * @throws ModuleDataException Major problem occurred. | |
156 | */ | |
157 | public void visitEnter(Import imp) throws ModuleDataException; | |
158 | ||
159 | /** | |
160 | * Visit certain element. Begin of visit. | |
161 | * | |
162 | * @param importList Begin visit of this element. | |
163 | * @throws ModuleDataException Major problem occurred. | |
164 | */ | |
165 | public void visitEnter(ImportList importList) throws ModuleDataException; | |
166 | ||
167 | /** | |
168 | * Visit certain element. Begin of visit. | |
169 | * | |
170 | * @param latex Begin visit of this element. | |
171 | * @throws ModuleDataException Major problem occurred. | |
172 | */ | |
173 | public void visitEnter(Latex latex) throws ModuleDataException; | |
174 | ||
175 | /** | |
176 | * Visit certain element. Begin of visit. | |
177 | * | |
178 | * @param latexList Begin visit of this element. | |
179 | * @throws ModuleDataException Major problem occurred. | |
180 | */ | |
181 | public void visitEnter(LatexList latexList) throws ModuleDataException; | |
182 | ||
183 | /** | |
184 | * Visit certain element. Begin of visit. | |
185 | * | |
186 | * @param linkList Begin visit of this element. | |
187 | * @throws ModuleDataException Major problem occurred. | |
188 | */ | |
189 | public void visitEnter(LinkList linkList) throws ModuleDataException; | |
190 | ||
191 | /** | |
192 | * Visit certain element. Begin of visit. | |
193 | * | |
194 | * @param literatureItem Begin visit of this element. | |
195 | * @throws ModuleDataException Major problem occurred. | |
196 | */ | |
197 | public void visitEnter(LiteratureItem literatureItem) throws ModuleDataException; | |
198 | ||
199 | /** | |
200 | * Visit certain element. Begin of visit. | |
201 | * | |
202 | * @param literatureItemList Begin visit of this element. | |
203 | * @throws ModuleDataException Major problem occurred. | |
204 | */ | |
205 | public void visitEnter(LiteratureItemList literatureItemList) throws ModuleDataException; | |
206 | ||
207 | /** | |
208 | * Visit certain element. Begin of visit. | |
209 | * | |
210 | * @param location Begin visit of this element. | |
211 | * @throws ModuleDataException Major problem occurred. | |
212 | */ | |
213 | public void visitEnter(Location location) throws ModuleDataException; | |
214 | ||
215 | /** | |
216 | * Visit certain element. Begin of visit. | |
217 | * | |
218 | * @param locationList Begin visit of this element. | |
219 | * @throws ModuleDataException Major problem occurred. | |
220 | */ | |
221 | public void visitEnter(LocationList locationList) throws ModuleDataException; | |
222 | ||
223 | /** | |
224 | * Visit certain element. Begin of visit. | |
225 | * | |
226 | * @param node Begin visit of this element. | |
227 | * @throws ModuleDataException Major problem occurred. | |
228 | */ | |
229 | public void visitEnter(Node node) throws ModuleDataException; | |
230 | ||
231 | /** | |
232 | * Visit certain element. Begin of visit. | |
233 | * | |
234 | * @param predicateDefinition Begin visit of this element. | |
235 | * @throws ModuleDataException Major problem occurred. | |
236 | */ | |
237 | public void visitEnter(InitialPredicateDefinition predicateDefinition) throws ModuleDataException; | |
238 | ||
239 | /** | |
240 | * Visit certain element. Begin of visit. | |
241 | * | |
242 | * @param predicateDefinition Begin visit of this element. | |
243 | * @throws ModuleDataException Major problem occurred. | |
244 | */ | |
245 | public void visitEnter(PredicateDefinition predicateDefinition) throws ModuleDataException; | |
246 | ||
247 | /** | |
248 | * Visit certain element. Begin of visit. | |
249 | * | |
250 | * @param proof Begin visit of this element. | |
251 | * @throws ModuleDataException Major problem occurred. | |
252 | */ | |
253 | public void visitEnter(FormalProof proof) throws ModuleDataException; | |
254 | ||
255 | /** | |
256 | * Visit certain element. Begin of visit. | |
257 | * | |
258 | * @param proofList Begin visit of this element. | |
259 | * @throws ModuleDataException Major problem occurred. | |
260 | */ | |
261 | public void visitEnter(FormalProofList proofList) throws ModuleDataException; | |
262 | ||
263 | /** | |
264 | * Visit formal proof line (but not an conditional proof line). | |
265 | * | |
266 | * @param proofLine Begin visit of this element. | |
267 | * @throws ModuleDataException Major problem occurred. | |
268 | */ | |
269 | public void visitEnter(FormalProofLine proofLine) throws ModuleDataException; | |
270 | ||
271 | /** | |
272 | * Visit certain element. Begin of visit. | |
273 | * | |
274 | * @param reason End visit of this element. | |
275 | * @throws ModuleDataException Major problem occurred. | |
276 | */ | |
277 | public void visitEnter(Reason reason) throws ModuleDataException; | |
278 | ||
279 | /** | |
280 | * Visit certain element. Begin of visit. | |
281 | * | |
282 | * @param reason Begin visit of this element. | |
283 | * @throws ModuleDataException Major problem occurred. | |
284 | */ | |
285 | public void visitEnter(ModusPonens reason) throws ModuleDataException; | |
286 | ||
287 | /** | |
288 | * Visit certain element. Begin of visit. | |
289 | * | |
290 | * @param reason Begin visit of this element. | |
291 | * @throws ModuleDataException Major problem occurred. | |
292 | */ | |
293 | public void visitEnter(Add reason) throws ModuleDataException; | |
294 | ||
295 | /** | |
296 | * Visit certain element. Begin of visit. | |
297 | * | |
298 | * @param reason Begin visit of this element. | |
299 | * @throws ModuleDataException Major problem occurred. | |
300 | */ | |
301 | public void visitEnter(Rename reason) throws ModuleDataException; | |
302 | ||
303 | /** | |
304 | * Visit certain element. Begin of visit. | |
305 | * | |
306 | * @param reason Begin visit of this element. | |
307 | * @throws ModuleDataException Major problem occurred. | |
308 | */ | |
309 | public void visitEnter(SubstFree reason) throws ModuleDataException; | |
310 | ||
311 | /** | |
312 | * Visit certain element. Begin of visit. | |
313 | * | |
314 | * @param reason Begin visit of this element. | |
315 | * @throws ModuleDataException Major problem occurred. | |
316 | */ | |
317 | public void visitEnter(SubstFunc reason) throws ModuleDataException; | |
318 | ||
319 | /** | |
320 | * Visit certain element. Begin of visit. | |
321 | * | |
322 | * @param reason Begin visit of this element. | |
323 | * @throws ModuleDataException Major problem occurred. | |
324 | */ | |
325 | public void visitEnter(SubstPred reason) throws ModuleDataException; | |
326 | ||
327 | /** | |
328 | * Visit certain element. Begin of visit. | |
329 | * | |
330 | * @param reason Begin visit of this element. | |
331 | * @throws ModuleDataException Major problem occurred. | |
332 | */ | |
333 | public void visitEnter(Existential reason) throws ModuleDataException; | |
334 | ||
335 | /** | |
336 | * Visit certain element. Begin of visit. | |
337 | * | |
338 | * @param reason Begin visit of this element. | |
339 | * @throws ModuleDataException Major problem occurred. | |
340 | */ | |
341 | public void visitEnter(Universal reason) throws ModuleDataException; | |
342 | ||
343 | /** | |
344 | * Visit conditional proof line. | |
345 | * | |
346 | * @param reason Begin visit of this element. | |
347 | * @throws ModuleDataException Major problem occurred. | |
348 | */ | |
349 | public void visitEnter(ConditionalProof reason) throws ModuleDataException; | |
350 | ||
351 | /** | |
352 | * Visit certain element. Begin of visit. | |
353 | * | |
354 | * @param hypothesis Begin visit of this element. | |
355 | * @throws ModuleDataException Major problem occurred. | |
356 | */ | |
357 | public void visitEnter(Hypothesis hypothesis) throws ModuleDataException; | |
358 | ||
359 | /** | |
360 | * Visit certain element. Begin of visit. | |
361 | * | |
362 | * @param conclusion Begin visit of this element. | |
363 | * @throws ModuleDataException Major problem occurred. | |
364 | */ | |
365 | public void visitEnter(Conclusion conclusion) throws ModuleDataException; | |
366 | ||
367 | /** | |
368 | * Visit certain element. Begin of visit. | |
369 | * | |
370 | * @param proofLineList Begin visit of this element. | |
371 | * @throws ModuleDataException Major problem occurred. | |
372 | */ | |
373 | public void visitEnter(FormalProofLineList proofLineList) throws ModuleDataException; | |
374 | ||
375 | /** | |
376 | * Visit certain element. Begin of visit. | |
377 | * | |
378 | * @param proof Begin visit of this element. | |
379 | * @throws ModuleDataException Major problem occurred. | |
380 | */ | |
381 | public void visitEnter(Proof proof) throws ModuleDataException; | |
382 | ||
383 | /** | |
384 | * Visit certain element. Begin of visit. | |
385 | * | |
386 | * @param proofList Begin visit of this element. | |
387 | * @throws ModuleDataException Major problem occurred. | |
388 | */ | |
389 | public void visitEnter(ProofList proofList) throws ModuleDataException; | |
390 | ||
391 | /** | |
392 | * Visit certain element. Begin of visit. | |
393 | * | |
394 | * @param proposition Begin visit of this element. | |
395 | * @throws ModuleDataException Major problem occurred. | |
396 | */ | |
397 | public void visitEnter(Proposition proposition) throws ModuleDataException; | |
398 | ||
399 | /** | |
400 | * Visit certain element. Begin of visit. | |
401 | * | |
402 | * @param qedeq Begin visit of this element. | |
403 | * @throws ModuleDataException Major problem occurred. | |
404 | */ | |
405 | public void visitEnter(Qedeq qedeq) throws ModuleDataException; | |
406 | ||
407 | /** | |
408 | * Visit certain element. Begin of visit. | |
409 | * | |
410 | * @param rule Begin visit of this element. | |
411 | * @throws ModuleDataException Major problem occurred. | |
412 | */ | |
413 | public void visitEnter(Rule rule) throws ModuleDataException; | |
414 | ||
415 | /** | |
416 | * Visit certain element. Begin of visit. | |
417 | * | |
418 | * @param list Begin visit of this element. | |
419 | * @throws ModuleDataException Major problem occurred. | |
420 | */ | |
421 | public void visitEnter(ChangedRuleList list) throws ModuleDataException; | |
422 | ||
423 | /** | |
424 | * Visit certain element. Begin of visit. | |
425 | * | |
426 | * @param rule Begin visit of this element. | |
427 | * @throws ModuleDataException Major problem occurred. | |
428 | */ | |
429 | public void visitEnter(ChangedRule rule) throws ModuleDataException; | |
430 | ||
431 | /** | |
432 | * Visit certain element. Begin of visit. | |
433 | * | |
434 | * @param section Begin visit of this element. | |
435 | * @throws ModuleDataException Major problem occurred. | |
436 | */ | |
437 | public void visitEnter(Section section) throws ModuleDataException; | |
438 | ||
439 | /** | |
440 | * Visit certain element. Begin of visit. | |
441 | * | |
442 | * @param sectionList Begin visit of this element. | |
443 | * @throws ModuleDataException Major problem occurred. | |
444 | */ | |
445 | public void visitEnter(SectionList sectionList) throws ModuleDataException; | |
446 | ||
447 | /** | |
448 | * Visit certain element. Begin of visit. | |
449 | * | |
450 | * @param specification Begin visit of this element. | |
451 | * @throws ModuleDataException Major problem occurred. | |
452 | */ | |
453 | public void visitEnter(Specification specification) throws ModuleDataException; | |
454 | ||
455 | /** | |
456 | * Visit certain element. Begin of visit. | |
457 | * | |
458 | * @param subsection Begin visit of this element. | |
459 | * @throws ModuleDataException Major problem occurred. | |
460 | */ | |
461 | public void visitEnter(Subsection subsection) throws ModuleDataException; | |
462 | ||
463 | /** | |
464 | * Visit certain element. Begin of visit. | |
465 | * | |
466 | * @param subsectionList Begin visit of this element. | |
467 | * @throws ModuleDataException Major problem occurred. | |
468 | */ | |
469 | public void visitEnter(SubsectionList subsectionList) throws ModuleDataException; | |
470 | ||
471 | /** | |
472 | * Visit certain element. Begin of visit. | |
473 | * | |
474 | * @param subsectionType Begin visit of this element. | |
475 | * @throws ModuleDataException Major problem occurred. | |
476 | */ | |
477 | public void visitEnter(SubsectionType subsectionType) throws ModuleDataException; | |
478 | ||
479 | /** | |
480 | * Visit certain element. Begin of visit. | |
481 | * | |
482 | * @param term Begin visit of this element. | |
483 | * @throws ModuleDataException Major problem occurred. | |
484 | */ | |
485 | public void visitEnter(Term term) throws ModuleDataException; | |
486 | ||
487 | /** | |
488 | * Visit certain element. Begin of visit. | |
489 | * | |
490 | * @param usedByList Begin visit of this element. | |
491 | * @throws ModuleDataException Major problem occurred. | |
492 | */ | |
493 | public void visitEnter(UsedByList usedByList) throws ModuleDataException; | |
494 | ||
495 | /** | |
496 | * Visit certain element. End of visit. | |
497 | * | |
498 | * @param author End visit of this element. | |
499 | * @throws ModuleDataException Major problem occurred. | |
500 | */ | |
501 | public void visitLeave(Author author) throws ModuleDataException; | |
502 | ||
503 | /** | |
504 | * Visit certain element. End of visit. | |
505 | * | |
506 | * @param authorList End visit of this element. | |
507 | * @throws ModuleDataException Major problem occurred. | |
508 | */ | |
509 | public void visitLeave(AuthorList authorList) throws ModuleDataException; | |
510 | ||
511 | /** | |
512 | * Visit certain element. End of visit. | |
513 | * | |
514 | * @param axiom End visit of this element. | |
515 | * @throws ModuleDataException Major problem occurred. | |
516 | */ | |
517 | public void visitLeave(Axiom axiom) throws ModuleDataException; | |
518 | ||
519 | /** | |
520 | * Visit certain element. End of visit. | |
521 | * | |
522 | * @param chapter End visit of this element. | |
523 | * @throws ModuleDataException Major problem occurred. | |
524 | */ | |
525 | public void visitLeave(Chapter chapter) throws ModuleDataException; | |
526 | ||
527 | /** | |
528 | * Visit certain element. End of visit. | |
529 | * | |
530 | * @param chapterList End visit of this element. | |
531 | * @throws ModuleDataException Major problem occurred. | |
532 | */ | |
533 | public void visitLeave(ChapterList chapterList) throws ModuleDataException; | |
534 | ||
535 | /** | |
536 | * Visit certain element. End of visit. | |
537 | * | |
538 | * @param formula End visit of this element. | |
539 | * @throws ModuleDataException Major problem occurred. | |
540 | */ | |
541 | public void visitLeave(Formula formula) throws ModuleDataException; | |
542 | ||
543 | /** | |
544 | * Visit certain element. End of visit. | |
545 | * | |
546 | * @param functionDefinition End visit of this element. | |
547 | * @throws ModuleDataException Major problem occurred. | |
548 | */ | |
549 | public void visitLeave(InitialFunctionDefinition functionDefinition) throws ModuleDataException; | |
550 | ||
551 | /** | |
552 | * Visit certain element. End of visit. | |
553 | * | |
554 | * @param functionDefinition End visit of this element. | |
555 | * @throws ModuleDataException Major problem occurred. | |
556 | */ | |
557 | public void visitLeave(FunctionDefinition functionDefinition) throws ModuleDataException; | |
558 | ||
559 | /** | |
560 | * Visit certain element. End of visit. | |
561 | * | |
562 | * @param header End visit of this element. | |
563 | * @throws ModuleDataException Major problem occurred. | |
564 | */ | |
565 | public void visitLeave(Header header) throws ModuleDataException; | |
566 | ||
567 | /** | |
568 | * Visit certain element. End of visit. | |
569 | * | |
570 | * @param imp End visit of this element. | |
571 | * @throws ModuleDataException Major problem occurred. | |
572 | */ | |
573 | public void visitLeave(Import imp) throws ModuleDataException; | |
574 | ||
575 | /** | |
576 | * Visit certain element. End of visit. | |
577 | * | |
578 | * @param importList End visit of this element. | |
579 | * @throws ModuleDataException Major problem occurred. | |
580 | */ | |
581 | public void visitLeave(ImportList importList) throws ModuleDataException; | |
582 | ||
583 | /** | |
584 | * Visit certain element. End of visit. | |
585 | * | |
586 | * @param latex End visit of this element. | |
587 | * @throws ModuleDataException Major problem occurred. | |
588 | */ | |
589 | public void visitLeave(Latex latex) throws ModuleDataException; | |
590 | ||
591 | /** | |
592 | * Visit certain element. End of visit. | |
593 | * | |
594 | * @param latexList End visit of this element. | |
595 | * @throws ModuleDataException Major problem occurred. | |
596 | */ | |
597 | public void visitLeave(LatexList latexList) throws ModuleDataException; | |
598 | ||
599 | /** | |
600 | * Visit certain element. End of visit. | |
601 | * | |
602 | * @param linkList End visit of this element. | |
603 | * @throws ModuleDataException Major problem occurred. | |
604 | */ | |
605 | public void visitLeave(LinkList linkList) throws ModuleDataException; | |
606 | ||
607 | /** | |
608 | * Visit certain element. End of visit. | |
609 | * | |
610 | * @param literatureItem End visit of this element. | |
611 | * @throws ModuleDataException Major problem occurred. | |
612 | */ | |
613 | public void visitLeave(LiteratureItem literatureItem) throws ModuleDataException; | |
614 | ||
615 | /** | |
616 | * Visit certain element. End of visit. | |
617 | * | |
618 | * @param literatureItemList End visit of this element. | |
619 | * @throws ModuleDataException Major problem occurred. | |
620 | */ | |
621 | public void visitLeave(LiteratureItemList literatureItemList) throws ModuleDataException; | |
622 | ||
623 | /** | |
624 | * Visit certain element. End of visit. | |
625 | * | |
626 | * @param location End visit of this element. | |
627 | * @throws ModuleDataException Major problem occurred. | |
628 | */ | |
629 | public void visitLeave(Location location) throws ModuleDataException; | |
630 | ||
631 | /** | |
632 | * Visit certain element. End of visit. | |
633 | * | |
634 | * @param locationList End visit of this element. | |
635 | * @throws ModuleDataException Major problem occurred. | |
636 | */ | |
637 | public void visitLeave(LocationList locationList) throws ModuleDataException; | |
638 | ||
639 | /** | |
640 | * Visit certain element. End of visit. | |
641 | * | |
642 | * @param node End visit of this element. | |
643 | * @throws ModuleDataException Major problem occurred. | |
644 | */ | |
645 | public void visitLeave(Node node) throws ModuleDataException; | |
646 | ||
647 | /** | |
648 | * Visit certain element. End of visit. | |
649 | * | |
650 | * @param predicateDefinition End visit of this element. | |
651 | * @throws ModuleDataException Major problem occurred. | |
652 | */ | |
653 | public void visitLeave(InitialPredicateDefinition predicateDefinition) throws ModuleDataException; | |
654 | ||
655 | /** | |
656 | * Visit certain element. End of visit. | |
657 | * | |
658 | * @param predicateDefinition End visit of this element. | |
659 | * @throws ModuleDataException Major problem occurred. | |
660 | */ | |
661 | public void visitLeave(PredicateDefinition predicateDefinition) throws ModuleDataException; | |
662 | ||
663 | /** | |
664 | * Visit certain element. End of visit. | |
665 | * | |
666 | * @param proofList End visit of this element. | |
667 | * @throws ModuleDataException Major problem occurred. | |
668 | */ | |
669 | public void visitLeave(FormalProofList proofList) throws ModuleDataException; | |
670 | ||
671 | /** | |
672 | * Visit certain element. End of visit. | |
673 | * | |
674 | * @param proof End visit of this element. | |
675 | * @throws ModuleDataException Major problem occurred. | |
676 | */ | |
677 | public void visitLeave(FormalProof proof) throws ModuleDataException; | |
678 | ||
679 | /** | |
680 | * Visit certain element. End of visit. | |
681 | * | |
682 | * @param proofLine End visit of this element. | |
683 | * @throws ModuleDataException Major problem occurred. | |
684 | */ | |
685 | public void visitLeave(FormalProofLine proofLine) throws ModuleDataException; | |
686 | ||
687 | /** | |
688 | * Visit certain element. End of visit. | |
689 | * | |
690 | * @param reason End visit of this element. | |
691 | * @throws ModuleDataException Major problem occurred. | |
692 | */ | |
693 | public void visitLeave(Reason reason) throws ModuleDataException; | |
694 | ||
695 | /** | |
696 | * Visit certain element. End of visit. | |
697 | * | |
698 | * @param proofLineList End visit of this element. | |
699 | * @throws ModuleDataException Major problem occurred. | |
700 | */ | |
701 | public void visitLeave(FormalProofLineList proofLineList) throws ModuleDataException; | |
702 | ||
703 | /** | |
704 | * Visit certain element. End of visit. | |
705 | * | |
706 | * @param reason End visit of this element. | |
707 | * @throws ModuleDataException Major problem occurred. | |
708 | */ | |
709 | public void visitLeave(ModusPonens reason) throws ModuleDataException; | |
710 | ||
711 | /** | |
712 | * Visit certain element. End of visit. | |
713 | * | |
714 | * @param reason End visit of this element. | |
715 | * @throws ModuleDataException Major problem occurred. | |
716 | */ | |
717 | public void visitLeave(Add reason) throws ModuleDataException; | |
718 | ||
719 | /** | |
720 | * Visit certain element. End of visit. | |
721 | * | |
722 | * @param reason End visit of this element. | |
723 | * @throws ModuleDataException Major problem occurred. | |
724 | */ | |
725 | public void visitLeave(Rename reason) throws ModuleDataException; | |
726 | ||
727 | /** | |
728 | * Visit certain element. End of visit. | |
729 | * | |
730 | * @param reason End visit of this element. | |
731 | * @throws ModuleDataException Major problem occurred. | |
732 | */ | |
733 | public void visitLeave(SubstFree reason) throws ModuleDataException; | |
734 | ||
735 | /** | |
736 | * Visit certain element. End of visit. | |
737 | * | |
738 | * @param reason End visit of this element. | |
739 | * @throws ModuleDataException Major problem occurred. | |
740 | */ | |
741 | public void visitLeave(SubstFunc reason) throws ModuleDataException; | |
742 | ||
743 | /** | |
744 | * Visit certain element. End of visit. | |
745 | * | |
746 | * @param reason End visit of this element. | |
747 | * @throws ModuleDataException Major problem occurred. | |
748 | */ | |
749 | public void visitLeave(SubstPred reason) throws ModuleDataException; | |
750 | ||
751 | /** | |
752 | * Visit certain element. End of visit. | |
753 | * | |
754 | * @param reason End visit of this element. | |
755 | * @throws ModuleDataException Major problem occurred. | |
756 | */ | |
757 | public void visitLeave(Existential reason) throws ModuleDataException; | |
758 | ||
759 | /** | |
760 | * Visit certain element. End of visit. | |
761 | * | |
762 | * @param reason End visit of this element. | |
763 | * @throws ModuleDataException Major problem occurred. | |
764 | */ | |
765 | public void visitLeave(Universal reason) throws ModuleDataException; | |
766 | ||
767 | /** | |
768 | * Visit certain element. End of visit. | |
769 | * | |
770 | * @param reason End visit of this element. | |
771 | * @throws ModuleDataException Major problem occurred. | |
772 | */ | |
773 | public void visitLeave(ConditionalProof reason) throws ModuleDataException; | |
774 | ||
775 | /** | |
776 | * Visit certain element. End of visit. | |
777 | * | |
778 | * @param hypothesis End visit of this element. | |
779 | * @throws ModuleDataException Major problem occurred. | |
780 | */ | |
781 | public void visitLeave(Hypothesis hypothesis) throws ModuleDataException; | |
782 | ||
783 | /** | |
784 | * Visit certain element. End of visit. | |
785 | * | |
786 | * @param conclusion End visit of this element. | |
787 | * @throws ModuleDataException Major problem occurred. | |
788 | */ | |
789 | public void visitLeave(Conclusion conclusion) throws ModuleDataException; | |
790 | ||
791 | /** | |
792 | * Visit certain element. End of visit. | |
793 | * | |
794 | * @param proof End visit of this element. | |
795 | * @throws ModuleDataException Major problem occurred. | |
796 | */ | |
797 | public void visitLeave(Proof proof) throws ModuleDataException; | |
798 | ||
799 | /** | |
800 | * Visit certain element. End of visit. | |
801 | * | |
802 | * @param proofList End visit of this element. | |
803 | * @throws ModuleDataException Major problem occurred. | |
804 | */ | |
805 | public void visitLeave(ProofList proofList) throws ModuleDataException; | |
806 | ||
807 | /** | |
808 | * Visit certain element. End of visit. | |
809 | * | |
810 | * @param proposition End visit of this element. | |
811 | * @throws ModuleDataException Major problem occurred. | |
812 | */ | |
813 | public void visitLeave(Proposition proposition) throws ModuleDataException; | |
814 | ||
815 | /** | |
816 | * Visit certain element. End of visit. | |
817 | * | |
818 | * @param qedeq End visit of this element. | |
819 | * @throws ModuleDataException Major problem occurred. | |
820 | */ | |
821 | public void visitLeave(Qedeq qedeq) throws ModuleDataException; | |
822 | ||
823 | /** | |
824 | * Visit certain element. End of visit. | |
825 | * | |
826 | * @param rule End visit of this element. | |
827 | * @throws ModuleDataException Major problem occurred. | |
828 | */ | |
829 | public void visitLeave(Rule rule) throws ModuleDataException; | |
830 | ||
831 | /** | |
832 | * Visit certain element. End of visit. | |
833 | * | |
834 | * @param list End visit of this element. | |
835 | * @throws ModuleDataException Major problem occurred. | |
836 | */ | |
837 | public void visitLeave(ChangedRuleList list) throws ModuleDataException; | |
838 | ||
839 | /** | |
840 | * Visit certain element. End of visit. | |
841 | * | |
842 | * @param rule End visit of this element. | |
843 | * @throws ModuleDataException Major problem occurred. | |
844 | */ | |
845 | public void visitLeave(ChangedRule rule) throws ModuleDataException; | |
846 | ||
847 | /** | |
848 | * Visit certain element. End of visit. | |
849 | * | |
850 | * @param section End visit of this element. | |
851 | * @throws ModuleDataException Major problem occurred. | |
852 | */ | |
853 | public void visitLeave(Section section) throws ModuleDataException; | |
854 | ||
855 | /** | |
856 | * Visit certain element. End of visit. | |
857 | * | |
858 | * @param sectionList End visit of this element. | |
859 | * @throws ModuleDataException Major problem occurred. | |
860 | */ | |
861 | public void visitLeave(SectionList sectionList) throws ModuleDataException; | |
862 | ||
863 | /** | |
864 | * Visit certain element. End of visit. | |
865 | * | |
866 | * @param specification End visit of this element. | |
867 | * @throws ModuleDataException Major problem occurred. | |
868 | */ | |
869 | public void visitLeave(Specification specification) throws ModuleDataException; | |
870 | ||
871 | /** | |
872 | * Visit certain element. End of visit. | |
873 | * | |
874 | * @param subsection End visit of this element. | |
875 | * @throws ModuleDataException Major problem occurred. | |
876 | */ | |
877 | public void visitLeave(Subsection subsection) throws ModuleDataException; | |
878 | ||
879 | /** | |
880 | * Visit certain element. End of visit. | |
881 | * | |
882 | * @param subsectionList End visit of this element. | |
883 | * @throws ModuleDataException Major problem occurred. | |
884 | */ | |
885 | public void visitLeave(SubsectionList subsectionList) throws ModuleDataException; | |
886 | ||
887 | /** | |
888 | * Visit certain element. End of visit. | |
889 | * | |
890 | * @param subsectionType End visit of this element. | |
891 | * @throws ModuleDataException Major problem occurred. | |
892 | */ | |
893 | public void visitLeave(SubsectionType subsectionType) throws ModuleDataException; | |
894 | ||
895 | /** | |
896 | * Visit certain element. End of visit. | |
897 | * | |
898 | * @param term End visit of this element. | |
899 | * @throws ModuleDataException Major problem occurred. | |
900 | */ | |
901 | public void visitLeave(Term term) throws ModuleDataException; | |
902 | ||
903 | /** | |
904 | * Visit certain element. End of visit. | |
905 | * | |
906 | * @param usedByList End visit of this element. | |
907 | * @throws ModuleDataException Major problem occurred. | |
908 | */ | |
909 | public void visitLeave(UsedByList usedByList) throws ModuleDataException; | |
910 | ||
911 | ||
912 | } |
|