01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.proof;
12:
13: /** Encapsulates information describing changes to a proof tree, and
14: * used to notify proof tree listeners of the change.
15: */
16:
17: public class ProofTreeEvent {
18:
19: private Proof source;
20: private Node node;
21: private Goal goal;
22: private ListOfGoal goals = SLListOfGoal.EMPTY_LIST;
23:
24: /** Create ProofTreeEvent for an event that happens at
25: * the specified node. */
26: public ProofTreeEvent(Proof source, Node node) {
27: this .source = source;
28: this .node = node;
29: }
30:
31: /** Create ProofTreeEvent for an event that happens at
32: * no particular node. */
33: public ProofTreeEvent(Proof source) {
34: this .source = source;
35: }
36:
37: /** Create ProofTreeEvent for the event that happened to the
38: * given goal
39: */
40: public ProofTreeEvent(Proof source, Goal goal) {
41: this .source = source;
42: this .goal = goal;
43: }
44:
45: /** Create ProofTreeEvent for the event that affects the goals
46: * given in the list.
47: */
48: public ProofTreeEvent(Proof source, ListOfGoal goals) {
49: this .source = source;
50: this .goals = goals;
51: }
52:
53: public Node getNode() {
54: return node;
55: }
56:
57: public Proof getSource() {
58: return source;
59: }
60:
61: public Goal getGoal() {
62: return goal;
63: }
64:
65: public ListOfGoal getGoals() {
66: return goals;
67: }
68:
69: public String toString() {
70: return "ProofTreeEvent: " + ((node != null) ? "node " : "")
71: + ((goal != null) ? "goal " : "")
72: + ((goals != SLListOfGoal.EMPTY_LIST) ? "goals " : "");
73: }
74: }
|