001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2013, 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.common.ModuleDataException;
071
072 /**
073 * Here are all elements to visit assembled that can be visited within a QEDEQ module.
074 *
075 * @author Michael Meyling
076 */
077 public interface QedeqVisitor extends ListVisitor {
078
079 /**
080 * Visit certain element. Begin of visit.
081 *
082 * @param author Begin visit of this element.
083 * @throws ModuleDataException Major problem occurred.
084 */
085 public void visitEnter(Author author) throws ModuleDataException;
086
087 /**
088 * Visit certain element. Begin of visit.
089 *
090 * @param authorList Begin visit of this element.
091 * @throws ModuleDataException Major problem occurred.
092 */
093 public void visitEnter(AuthorList authorList) throws ModuleDataException;
094
095 /**
096 * Visit certain element. Begin of visit.
097 *
098 * @param axiom Begin visit of this element.
099 * @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 }
|