1 /* This file is part of the project "Hilbert II" - http://www.qedeq.org" target="alexandria_uri">http://www.qedeq.org 2 * 3 * Copyright 2000-2014, 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 }