001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2011, Michael Meyling <mime@qedeq.org>.
004 *
005 * "Hilbert II" is free software; you can redistribute
006 * it and/or modify it under the terms of the GNU General Public
007 * License as published by the Free Software Foundation; either
008 * version 2 of the License, or (at your option) any later version.
009 *
010 * This program is distributed in the hope that it will be useful,
011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013 * GNU General Public License for more details.
014 */
015
016 package org.qedeq.kernel.se.visitor;
017
018 import org.qedeq.kernel.se.base.module.Add;
019 import org.qedeq.kernel.se.base.module.Author;
020 import org.qedeq.kernel.se.base.module.AuthorList;
021 import org.qedeq.kernel.se.base.module.Axiom;
022 import org.qedeq.kernel.se.base.module.ChangedRule;
023 import org.qedeq.kernel.se.base.module.ChangedRuleList;
024 import org.qedeq.kernel.se.base.module.Chapter;
025 import org.qedeq.kernel.se.base.module.ChapterList;
026 import org.qedeq.kernel.se.base.module.Conclusion;
027 import org.qedeq.kernel.se.base.module.ConditionalProof;
028 import org.qedeq.kernel.se.base.module.Existential;
029 import org.qedeq.kernel.se.base.module.FormalProof;
030 import org.qedeq.kernel.se.base.module.FormalProofLine;
031 import org.qedeq.kernel.se.base.module.FormalProofLineList;
032 import org.qedeq.kernel.se.base.module.FormalProofList;
033 import org.qedeq.kernel.se.base.module.Formula;
034 import org.qedeq.kernel.se.base.module.FunctionDefinition;
035 import org.qedeq.kernel.se.base.module.Header;
036 import org.qedeq.kernel.se.base.module.Hypothesis;
037 import org.qedeq.kernel.se.base.module.Import;
038 import org.qedeq.kernel.se.base.module.ImportList;
039 import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
040 import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
041 import org.qedeq.kernel.se.base.module.Latex;
042 import org.qedeq.kernel.se.base.module.LatexList;
043 import org.qedeq.kernel.se.base.module.LinkList;
044 import org.qedeq.kernel.se.base.module.LiteratureItem;
045 import org.qedeq.kernel.se.base.module.LiteratureItemList;
046 import org.qedeq.kernel.se.base.module.Location;
047 import org.qedeq.kernel.se.base.module.LocationList;
048 import org.qedeq.kernel.se.base.module.ModusPonens;
049 import org.qedeq.kernel.se.base.module.Node;
050 import org.qedeq.kernel.se.base.module.PredicateDefinition;
051 import org.qedeq.kernel.se.base.module.Proof;
052 import org.qedeq.kernel.se.base.module.ProofList;
053 import org.qedeq.kernel.se.base.module.Proposition;
054 import org.qedeq.kernel.se.base.module.Qedeq;
055 import org.qedeq.kernel.se.base.module.Reason;
056 import org.qedeq.kernel.se.base.module.Rename;
057 import org.qedeq.kernel.se.base.module.Rule;
058 import org.qedeq.kernel.se.base.module.Section;
059 import org.qedeq.kernel.se.base.module.SectionList;
060 import org.qedeq.kernel.se.base.module.Specification;
061 import org.qedeq.kernel.se.base.module.Subsection;
062 import org.qedeq.kernel.se.base.module.SubsectionList;
063 import org.qedeq.kernel.se.base.module.SubsectionType;
064 import org.qedeq.kernel.se.base.module.SubstFree;
065 import org.qedeq.kernel.se.base.module.SubstFunc;
066 import org.qedeq.kernel.se.base.module.SubstPred;
067 import org.qedeq.kernel.se.base.module.Term;
068 import org.qedeq.kernel.se.base.module.Universal;
069 import org.qedeq.kernel.se.base.module.UsedByList;
070 import org.qedeq.kernel.se.base.module.VariableList;
071 import org.qedeq.kernel.se.common.ModuleDataException;
072
073 /**
074 * Here are all elements to visit assembled that can be visited within a QEDEQ module.
075 *
076 * @author Michael Meyling
077 */
078 public interface QedeqVisitor extends ListVisitor {
079
080 /**
081 * Visit certain element. Begin of visit.
082 *
083 * @param author Begin visit of this element.
084 * @throws ModuleDataException Major problem occurred.
085 */
086 public void visitEnter(Author author) throws ModuleDataException;
087
088 /**
089 * Visit certain element. Begin of visit.
090 *
091 * @param authorList Begin visit of this element.
092 * @throws ModuleDataException Major problem occurred.
093 */
094 public void visitEnter(AuthorList authorList) throws ModuleDataException;
095
096 /**
097 * Visit certain element. Begin of visit.
098 *
099 * @param axiom Begin visit of this element.
100 * @throws ModuleDataException Major problem occurred.
101 */
102 public void visitEnter(Axiom axiom) throws ModuleDataException;
103
104 /**
105 * Visit certain element. Begin of visit.
106 *
107 * @param chapter Begin visit of this element.
108 * @throws ModuleDataException Major problem occurred.
109 */
110 public void visitEnter(Chapter chapter) throws ModuleDataException;
111
112 /**
113 * Visit certain element. Begin of visit.
114 *
115 * @param chapterList Begin visit of this element.
116 * @throws ModuleDataException Major problem occurred.
117 */
118 public void visitEnter(ChapterList chapterList) throws ModuleDataException;
119
120 /**
121 * Visit certain element. Begin of visit.
122 *
123 * @param formula Begin visit of this element.
124 * @throws ModuleDataException Major problem occurred.
125 */
126 public void visitEnter(Formula formula) throws ModuleDataException;
127
128 /**
129 * Visit certain element. Begin of visit.
130 *
131 * @param functionDefinition Begin visit of this element.
132 * @throws ModuleDataException Major problem occurred.
133 */
134 public void visitEnter(InitialFunctionDefinition functionDefinition) throws ModuleDataException;
135
136 /**
137 * Visit certain element. Begin of visit.
138 *
139 * @param functionDefinition Begin visit of this element.
140 * @throws ModuleDataException Major problem occurred.
141 */
142 public void visitEnter(FunctionDefinition functionDefinition) throws ModuleDataException;
143
144 /**
145 * Visit certain element. Begin of visit.
146 *
147 * @param header Begin visit of this element.
148 * @throws ModuleDataException Major problem occurred.
149 */
150 public void visitEnter(Header header) throws ModuleDataException;
151
152 /**
153 * Visit certain element. Begin of visit.
154 *
155 * @param imp Begin visit of this element.
156 * @throws ModuleDataException Major problem occurred.
157 */
158 public void visitEnter(Import imp) throws ModuleDataException;
159
160 /**
161 * Visit certain element. Begin of visit.
162 *
163 * @param importList Begin visit of this element.
164 * @throws ModuleDataException Major problem occurred.
165 */
166 public void visitEnter(ImportList importList) throws ModuleDataException;
167
168 /**
169 * Visit certain element. Begin of visit.
170 *
171 * @param latex Begin visit of this element.
172 * @throws ModuleDataException Major problem occurred.
173 */
174 public void visitEnter(Latex latex) throws ModuleDataException;
175
176 /**
177 * Visit certain element. Begin of visit.
178 *
179 * @param latexList Begin visit of this element.
180 * @throws ModuleDataException Major problem occurred.
181 */
182 public void visitEnter(LatexList latexList) throws ModuleDataException;
183
184 /**
185 * Visit certain element. Begin of visit.
186 *
187 * @param linkList Begin visit of this element.
188 * @throws ModuleDataException Major problem occurred.
189 */
190 public void visitEnter(LinkList linkList) throws ModuleDataException;
191
192 /**
193 * Visit certain element. Begin of visit.
194 *
195 * @param literatureItem Begin visit of this element.
196 * @throws ModuleDataException Major problem occurred.
197 */
198 public void visitEnter(LiteratureItem literatureItem) throws ModuleDataException;
199
200 /**
201 * Visit certain element. Begin of visit.
202 *
203 * @param literatureItemList Begin visit of this element.
204 * @throws ModuleDataException Major problem occurred.
205 */
206 public void visitEnter(LiteratureItemList literatureItemList) throws ModuleDataException;
207
208 /**
209 * Visit certain element. Begin of visit.
210 *
211 * @param location Begin visit of this element.
212 * @throws ModuleDataException Major problem occurred.
213 */
214 public void visitEnter(Location location) throws ModuleDataException;
215
216 /**
217 * Visit certain element. Begin of visit.
218 *
219 * @param locationList Begin visit of this element.
220 * @throws ModuleDataException Major problem occurred.
221 */
222 public void visitEnter(LocationList locationList) throws ModuleDataException;
223
224 /**
225 * Visit certain element. Begin of visit.
226 *
227 * @param node Begin visit of this element.
228 * @throws ModuleDataException Major problem occurred.
229 */
230 public void visitEnter(Node node) throws ModuleDataException;
231
232 /**
233 * Visit certain element. Begin of visit.
234 *
235 * @param predicateDefinition Begin visit of this element.
236 * @throws ModuleDataException Major problem occurred.
237 */
238 public void visitEnter(InitialPredicateDefinition predicateDefinition) throws ModuleDataException;
239
240 /**
241 * Visit certain element. Begin of visit.
242 *
243 * @param predicateDefinition Begin visit of this element.
244 * @throws ModuleDataException Major problem occurred.
245 */
246 public void visitEnter(PredicateDefinition predicateDefinition) throws ModuleDataException;
247
248 /**
249 * Visit certain element. Begin of visit.
250 *
251 * @param proof Begin visit of this element.
252 * @throws ModuleDataException Major problem occurred.
253 */
254 public void visitEnter(FormalProof proof) throws ModuleDataException;
255
256 /**
257 * Visit certain element. Begin of visit.
258 *
259 * @param proofList Begin visit of this element.
260 * @throws ModuleDataException Major problem occurred.
261 */
262 public void visitEnter(FormalProofList proofList) throws ModuleDataException;
263
264 /**
265 * Visit formal proof line (but not an conditional proof line).
266 *
267 * @param proofLine Begin visit of this element.
268 * @throws ModuleDataException Major problem occurred.
269 */
270 public void visitEnter(FormalProofLine proofLine) throws ModuleDataException;
271
272 /**
273 * Visit certain element. Begin of visit.
274 *
275 * @param reason End visit of this element.
276 * @throws ModuleDataException Major problem occurred.
277 */
278 public void visitEnter(Reason reason) throws ModuleDataException;
279
280 /**
281 * Visit certain element. Begin of visit.
282 *
283 * @param reason Begin visit of this element.
284 * @throws ModuleDataException Major problem occurred.
285 */
286 public void visitEnter(ModusPonens reason) throws ModuleDataException;
287
288 /**
289 * Visit certain element. Begin of visit.
290 *
291 * @param reason Begin visit of this element.
292 * @throws ModuleDataException Major problem occurred.
293 */
294 public void visitEnter(Add reason) throws ModuleDataException;
295
296 /**
297 * Visit certain element. Begin of visit.
298 *
299 * @param reason Begin visit of this element.
300 * @throws ModuleDataException Major problem occurred.
301 */
302 public void visitEnter(Rename reason) throws ModuleDataException;
303
304 /**
305 * Visit certain element. Begin of visit.
306 *
307 * @param reason Begin visit of this element.
308 * @throws ModuleDataException Major problem occurred.
309 */
310 public void visitEnter(SubstFree reason) throws ModuleDataException;
311
312 /**
313 * Visit certain element. Begin of visit.
314 *
315 * @param reason Begin visit of this element.
316 * @throws ModuleDataException Major problem occurred.
317 */
318 public void visitEnter(SubstFunc reason) throws ModuleDataException;
319
320 /**
321 * Visit certain element. Begin of visit.
322 *
323 * @param reason Begin visit of this element.
324 * @throws ModuleDataException Major problem occurred.
325 */
326 public void visitEnter(SubstPred reason) throws ModuleDataException;
327
328 /**
329 * Visit certain element. Begin of visit.
330 *
331 * @param reason Begin visit of this element.
332 * @throws ModuleDataException Major problem occurred.
333 */
334 public void visitEnter(Existential reason) throws ModuleDataException;
335
336 /**
337 * Visit certain element. Begin of visit.
338 *
339 * @param reason Begin visit of this element.
340 * @throws ModuleDataException Major problem occurred.
341 */
342 public void visitEnter(Universal reason) throws ModuleDataException;
343
344 /**
345 * Visit conditional proof line.
346 *
347 * @param reason Begin visit of this element.
348 * @throws ModuleDataException Major problem occurred.
349 */
350 public void visitEnter(ConditionalProof reason) throws ModuleDataException;
351
352 /**
353 * Visit certain element. Begin of visit.
354 *
355 * @param hypothesis Begin visit of this element.
356 * @throws ModuleDataException Major problem occurred.
357 */
358 public void visitEnter(Hypothesis hypothesis) throws ModuleDataException;
359
360 /**
361 * Visit certain element. Begin of visit.
362 *
363 * @param conclusion Begin visit of this element.
364 * @throws ModuleDataException Major problem occurred.
365 */
366 public void visitEnter(Conclusion conclusion) throws ModuleDataException;
367
368 /**
369 * Visit certain element. Begin of visit.
370 *
371 * @param proofLineList Begin visit of this element.
372 * @throws ModuleDataException Major problem occurred.
373 */
374 public void visitEnter(FormalProofLineList proofLineList) throws ModuleDataException;
375
376 /**
377 * Visit certain element. Begin of visit.
378 *
379 * @param proof Begin visit of this element.
380 * @throws ModuleDataException Major problem occurred.
381 */
382 public void visitEnter(Proof proof) throws ModuleDataException;
383
384 /**
385 * Visit certain element. Begin of visit.
386 *
387 * @param proofList Begin visit of this element.
388 * @throws ModuleDataException Major problem occurred.
389 */
390 public void visitEnter(ProofList proofList) throws ModuleDataException;
391
392 /**
393 * Visit certain element. Begin of visit.
394 *
395 * @param proposition Begin visit of this element.
396 * @throws ModuleDataException Major problem occurred.
397 */
398 public void visitEnter(Proposition proposition) throws ModuleDataException;
399
400 /**
401 * Visit certain element. Begin of visit.
402 *
403 * @param qedeq Begin visit of this element.
404 * @throws ModuleDataException Major problem occurred.
405 */
406 public void visitEnter(Qedeq qedeq) throws ModuleDataException;
407
408 /**
409 * Visit certain element. Begin of visit.
410 *
411 * @param rule Begin visit of this element.
412 * @throws ModuleDataException Major problem occurred.
413 */
414 public void visitEnter(Rule rule) throws ModuleDataException;
415
416 /**
417 * Visit certain element. Begin of visit.
418 *
419 * @param list Begin visit of this element.
420 * @throws ModuleDataException Major problem occurred.
421 */
422 public void visitEnter(ChangedRuleList list) throws ModuleDataException;
423
424 /**
425 * Visit certain element. Begin of visit.
426 *
427 * @param rule Begin visit of this element.
428 * @throws ModuleDataException Major problem occurred.
429 */
430 public void visitEnter(ChangedRule rule) throws ModuleDataException;
431
432 /**
433 * Visit certain element. Begin of visit.
434 *
435 * @param section Begin visit of this element.
436 * @throws ModuleDataException Major problem occurred.
437 */
438 public void visitEnter(Section section) throws ModuleDataException;
439
440 /**
441 * Visit certain element. Begin of visit.
442 *
443 * @param sectionList Begin visit of this element.
444 * @throws ModuleDataException Major problem occurred.
445 */
446 public void visitEnter(SectionList sectionList) throws ModuleDataException;
447
448 /**
449 * Visit certain element. Begin of visit.
450 *
451 * @param specification Begin visit of this element.
452 * @throws ModuleDataException Major problem occurred.
453 */
454 public void visitEnter(Specification specification) throws ModuleDataException;
455
456 /**
457 * Visit certain element. Begin of visit.
458 *
459 * @param subsection Begin visit of this element.
460 * @throws ModuleDataException Major problem occurred.
461 */
462 public void visitEnter(Subsection subsection) throws ModuleDataException;
463
464 /**
465 * Visit certain element. Begin of visit.
466 *
467 * @param subsectionList Begin visit of this element.
468 * @throws ModuleDataException Major problem occurred.
469 */
470 public void visitEnter(SubsectionList subsectionList) throws ModuleDataException;
471
472 /**
473 * Visit certain element. Begin of visit.
474 *
475 * @param subsectionType Begin visit of this element.
476 * @throws ModuleDataException Major problem occurred.
477 */
478 public void visitEnter(SubsectionType subsectionType) throws ModuleDataException;
479
480 /**
481 * Visit certain element. Begin of visit.
482 *
483 * @param term Begin visit of this element.
484 * @throws ModuleDataException Major problem occurred.
485 */
486 public void visitEnter(Term term) throws ModuleDataException;
487
488 /**
489 * Visit certain element. Begin of visit.
490 *
491 * @param usedByList Begin visit of this element.
492 * @throws ModuleDataException Major problem occurred.
493 */
494 public void visitEnter(UsedByList usedByList) throws ModuleDataException;
495
496 /**
497 * Visit certain element. Begin of visit.
498 *
499 * @param variableList Begin visit of this element.
500 * @throws ModuleDataException Major problem occurred.
501 */
502 public void visitEnter(VariableList variableList) throws ModuleDataException;
503
504 /**
505 * Visit certain element. End of visit.
506 *
507 * @param author End visit of this element.
508 * @throws ModuleDataException Major problem occurred.
509 */
510 public void visitLeave(Author author) throws ModuleDataException;
511
512 /**
513 * Visit certain element. End of visit.
514 *
515 * @param authorList End visit of this element.
516 * @throws ModuleDataException Major problem occurred.
517 */
518 public void visitLeave(AuthorList authorList) throws ModuleDataException;
519
520 /**
521 * Visit certain element. End of visit.
522 *
523 * @param axiom End visit of this element.
524 * @throws ModuleDataException Major problem occurred.
525 */
526 public void visitLeave(Axiom axiom) throws ModuleDataException;
527
528 /**
529 * Visit certain element. End of visit.
530 *
531 * @param chapter End visit of this element.
532 * @throws ModuleDataException Major problem occurred.
533 */
534 public void visitLeave(Chapter chapter) throws ModuleDataException;
535
536 /**
537 * Visit certain element. End of visit.
538 *
539 * @param chapterList End visit of this element.
540 * @throws ModuleDataException Major problem occurred.
541 */
542 public void visitLeave(ChapterList chapterList) throws ModuleDataException;
543
544 /**
545 * Visit certain element. End of visit.
546 *
547 * @param formula End visit of this element.
548 * @throws ModuleDataException Major problem occurred.
549 */
550 public void visitLeave(Formula formula) throws ModuleDataException;
551
552 /**
553 * Visit certain element. End of visit.
554 *
555 * @param functionDefinition End visit of this element.
556 * @throws ModuleDataException Major problem occurred.
557 */
558 public void visitLeave(InitialFunctionDefinition functionDefinition) throws ModuleDataException;
559
560 /**
561 * Visit certain element. End of visit.
562 *
563 * @param functionDefinition End visit of this element.
564 * @throws ModuleDataException Major problem occurred.
565 */
566 public void visitLeave(FunctionDefinition functionDefinition) throws ModuleDataException;
567
568 /**
569 * Visit certain element. End of visit.
570 *
571 * @param header End visit of this element.
572 * @throws ModuleDataException Major problem occurred.
573 */
574 public void visitLeave(Header header) throws ModuleDataException;
575
576 /**
577 * Visit certain element. End of visit.
578 *
579 * @param imp End visit of this element.
580 * @throws ModuleDataException Major problem occurred.
581 */
582 public void visitLeave(Import imp) throws ModuleDataException;
583
584 /**
585 * Visit certain element. End of visit.
586 *
587 * @param importList End visit of this element.
588 * @throws ModuleDataException Major problem occurred.
589 */
590 public void visitLeave(ImportList importList) throws ModuleDataException;
591
592 /**
593 * Visit certain element. End of visit.
594 *
595 * @param latex End visit of this element.
596 * @throws ModuleDataException Major problem occurred.
597 */
598 public void visitLeave(Latex latex) throws ModuleDataException;
599
600 /**
601 * Visit certain element. End of visit.
602 *
603 * @param latexList End visit of this element.
604 * @throws ModuleDataException Major problem occurred.
605 */
606 public void visitLeave(LatexList latexList) throws ModuleDataException;
607
608 /**
609 * Visit certain element. End of visit.
610 *
611 * @param linkList End visit of this element.
612 * @throws ModuleDataException Major problem occurred.
613 */
614 public void visitLeave(LinkList linkList) throws ModuleDataException;
615
616 /**
617 * Visit certain element. End of visit.
618 *
619 * @param literatureItem End visit of this element.
620 * @throws ModuleDataException Major problem occurred.
621 */
622 public void visitLeave(LiteratureItem literatureItem) throws ModuleDataException;
623
624 /**
625 * Visit certain element. End of visit.
626 *
627 * @param literatureItemList End visit of this element.
628 * @throws ModuleDataException Major problem occurred.
629 */
630 public void visitLeave(LiteratureItemList literatureItemList) throws ModuleDataException;
631
632 /**
633 * Visit certain element. End of visit.
634 *
635 * @param location End visit of this element.
636 * @throws ModuleDataException Major problem occurred.
637 */
638 public void visitLeave(Location location) throws ModuleDataException;
639
640 /**
641 * Visit certain element. End of visit.
642 *
643 * @param locationList End visit of this element.
644 * @throws ModuleDataException Major problem occurred.
645 */
646 public void visitLeave(LocationList locationList) throws ModuleDataException;
647
648 /**
649 * Visit certain element. End of visit.
650 *
651 * @param authorList End visit of this element.
652 * @throws ModuleDataException Major problem occurred.
653 */
654 public void visitLeave(Node authorList) throws ModuleDataException;
655
656 /**
657 * Visit certain element. End of visit.
658 *
659 * @param predicateDefinition End visit of this element.
660 * @throws ModuleDataException Major problem occurred.
661 */
662 public void visitLeave(InitialPredicateDefinition predicateDefinition) throws ModuleDataException;
663
664 /**
665 * Visit certain element. End of visit.
666 *
667 * @param predicateDefinition End visit of this element.
668 * @throws ModuleDataException Major problem occurred.
669 */
670 public void visitLeave(PredicateDefinition predicateDefinition) throws ModuleDataException;
671
672 /**
673 * Visit certain element. End of visit.
674 *
675 * @param proofList End visit of this element.
676 * @throws ModuleDataException Major problem occurred.
677 */
678 public void visitLeave(FormalProofList proofList) throws ModuleDataException;
679
680 /**
681 * Visit certain element. End of visit.
682 *
683 * @param proof End visit of this element.
684 * @throws ModuleDataException Major problem occurred.
685 */
686 public void visitLeave(FormalProof proof) throws ModuleDataException;
687
688 /**
689 * Visit certain element. End of visit.
690 *
691 * @param proofLine End visit of this element.
692 * @throws ModuleDataException Major problem occurred.
693 */
694 public void visitLeave(FormalProofLine proofLine) throws ModuleDataException;
695
696 /**
697 * Visit certain element. End of visit.
698 *
699 * @param reason End visit of this element.
700 * @throws ModuleDataException Major problem occurred.
701 */
702 public void visitLeave(Reason reason) throws ModuleDataException;
703
704 /**
705 * Visit certain element. End of visit.
706 *
707 * @param proofLineList End visit of this element.
708 * @throws ModuleDataException Major problem occurred.
709 */
710 public void visitLeave(FormalProofLineList proofLineList) throws ModuleDataException;
711
712 /**
713 * Visit certain element. End of visit.
714 *
715 * @param reason End visit of this element.
716 * @throws ModuleDataException Major problem occurred.
717 */
718 public void visitLeave(ModusPonens reason) throws ModuleDataException;
719
720 /**
721 * Visit certain element. End of visit.
722 *
723 * @param reason End visit of this element.
724 * @throws ModuleDataException Major problem occurred.
725 */
726 public void visitLeave(Add reason) throws ModuleDataException;
727
728 /**
729 * Visit certain element. End of visit.
730 *
731 * @param reason End visit of this element.
732 * @throws ModuleDataException Major problem occurred.
733 */
734 public void visitLeave(Rename reason) throws ModuleDataException;
735
736 /**
737 * Visit certain element. End of visit.
738 *
739 * @param reason End visit of this element.
740 * @throws ModuleDataException Major problem occurred.
741 */
742 public void visitLeave(SubstFree reason) throws ModuleDataException;
743
744 /**
745 * Visit certain element. End of visit.
746 *
747 * @param reason End visit of this element.
748 * @throws ModuleDataException Major problem occurred.
749 */
750 public void visitLeave(SubstFunc reason) throws ModuleDataException;
751
752 /**
753 * Visit certain element. End of visit.
754 *
755 * @param reason End visit of this element.
756 * @throws ModuleDataException Major problem occurred.
757 */
758 public void visitLeave(SubstPred reason) throws ModuleDataException;
759
760 /**
761 * Visit certain element. End of visit.
762 *
763 * @param reason End visit of this element.
764 * @throws ModuleDataException Major problem occurred.
765 */
766 public void visitLeave(Existential reason) throws ModuleDataException;
767
768 /**
769 * Visit certain element. End of visit.
770 *
771 * @param reason End visit of this element.
772 * @throws ModuleDataException Major problem occurred.
773 */
774 public void visitLeave(Universal reason) throws ModuleDataException;
775
776 /**
777 * Visit certain element. End of visit.
778 *
779 * @param reason End visit of this element.
780 * @throws ModuleDataException Major problem occurred.
781 */
782 public void visitLeave(ConditionalProof reason) throws ModuleDataException;
783
784 /**
785 * Visit certain element. End of visit.
786 *
787 * @param hypothesis End visit of this element.
788 * @throws ModuleDataException Major problem occurred.
789 */
790 public void visitLeave(Hypothesis hypothesis) throws ModuleDataException;
791
792 /**
793 * Visit certain element. End of visit.
794 *
795 * @param conclusion End visit of this element.
796 * @throws ModuleDataException Major problem occurred.
797 */
798 public void visitLeave(Conclusion conclusion) throws ModuleDataException;
799
800 /**
801 * Visit certain element. End of visit.
802 *
803 * @param proof End visit of this element.
804 * @throws ModuleDataException Major problem occurred.
805 */
806 public void visitLeave(Proof proof) throws ModuleDataException;
807
808 /**
809 * Visit certain element. End of visit.
810 *
811 * @param proofList End visit of this element.
812 * @throws ModuleDataException Major problem occurred.
813 */
814 public void visitLeave(ProofList proofList) throws ModuleDataException;
815
816 /**
817 * Visit certain element. End of visit.
818 *
819 * @param proposition End visit of this element.
820 * @throws ModuleDataException Major problem occurred.
821 */
822 public void visitLeave(Proposition proposition) throws ModuleDataException;
823
824 /**
825 * Visit certain element. End of visit.
826 *
827 * @param qedeq End visit of this element.
828 * @throws ModuleDataException Major problem occurred.
829 */
830 public void visitLeave(Qedeq qedeq) throws ModuleDataException;
831
832 /**
833 * Visit certain element. End of visit.
834 *
835 * @param rule End visit of this element.
836 * @throws ModuleDataException Major problem occurred.
837 */
838 public void visitLeave(Rule rule) throws ModuleDataException;
839
840 /**
841 * Visit certain element. End of visit.
842 *
843 * @param list End visit of this element.
844 * @throws ModuleDataException Major problem occurred.
845 */
846 public void visitLeave(ChangedRuleList list) throws ModuleDataException;
847
848 /**
849 * Visit certain element. End of visit.
850 *
851 * @param rule End visit of this element.
852 * @throws ModuleDataException Major problem occurred.
853 */
854 public void visitLeave(ChangedRule rule) throws ModuleDataException;
855
856 /**
857 * Visit certain element. End of visit.
858 *
859 * @param section End visit of this element.
860 * @throws ModuleDataException Major problem occurred.
861 */
862 public void visitLeave(Section section) throws ModuleDataException;
863
864 /**
865 * Visit certain element. End of visit.
866 *
867 * @param sectionList End visit of this element.
868 * @throws ModuleDataException Major problem occurred.
869 */
870 public void visitLeave(SectionList sectionList) throws ModuleDataException;
871
872 /**
873 * Visit certain element. End of visit.
874 *
875 * @param specification End visit of this element.
876 * @throws ModuleDataException Major problem occurred.
877 */
878 public void visitLeave(Specification specification) throws ModuleDataException;
879
880 /**
881 * Visit certain element. End of visit.
882 *
883 * @param subsection End visit of this element.
884 * @throws ModuleDataException Major problem occurred.
885 */
886 public void visitLeave(Subsection subsection) throws ModuleDataException;
887
888 /**
889 * Visit certain element. End of visit.
890 *
891 * @param subsectionList End visit of this element.
892 * @throws ModuleDataException Major problem occurred.
893 */
894 public void visitLeave(SubsectionList subsectionList) throws ModuleDataException;
895
896 /**
897 * Visit certain element. End of visit.
898 *
899 * @param subsectionType End visit of this element.
900 * @throws ModuleDataException Major problem occurred.
901 */
902 public void visitLeave(SubsectionType subsectionType) throws ModuleDataException;
903
904 /**
905 * Visit certain element. End of visit.
906 *
907 * @param term End visit of this element.
908 * @throws ModuleDataException Major problem occurred.
909 */
910 public void visitLeave(Term term) throws ModuleDataException;
911
912 /**
913 * Visit certain element. End of visit.
914 *
915 * @param usedByList End visit of this element.
916 * @throws ModuleDataException Major problem occurred.
917 */
918 public void visitLeave(UsedByList usedByList) throws ModuleDataException;
919
920 /**
921 * Visit certain element. End of visit.
922 *
923 * @param variableList End visit of this element.
924 * @throws ModuleDataException Major problem occurred.
925 */
926 public void visitLeave(VariableList variableList) throws ModuleDataException;
927
928 }
|