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: import de.uka.ilkd.key.logic.SequentChangeInfo;
14:
15: /** interface to be implemented by a goal listener */
16: public interface GoalListener {
17:
18: /**
19: * informs the listener about a change that occured to the sequent of goal
20: */
21: void sequentChanged(Goal source, SequentChangeInfo sci);
22:
23: /**
24: * Informs the listener that the given goal <code>source</code>
25: * has been replaced by the goals <code>newGoals</code> (note that
26: * <code>source</code> may be an element of
27: * <code>newGoals</code>). The nodes of <code>newGoals</code> are
28: * children of the node <code>parent</code>
29: */
30: void goalReplaced(Goal source, Node parent, ListOfGoal newGoals);
31: }
|