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: public interface ProofTreeListener {
14:
15: /** The node mentioned in the ProofTreeEvent has changed, and/or
16: * there are new descendants of that node. Any nodes that are not
17: * descendants of that node are unaffected. */
18: void proofExpanded(ProofTreeEvent e);
19:
20: /** The proof tree has been pruned under the node mentioned in the
21: * ProofTreeEvent. In other words, that node should no longer
22: * have any children now. Any nodes that were not descendants of
23: * that node are unaffected.*/
24: void proofPruned(ProofTreeEvent e);
25:
26: /** The structure of the proof has changed radically. Any client should
27: * rescan the whole proof tree. */
28: void proofStructureChanged(ProofTreeEvent e);
29:
30: /** The proof trees has been closed (the list of goals is empty).
31: */
32: void proofClosed(ProofTreeEvent e);
33:
34: /** The goal mentioned in the ProofEvent has been removed
35: *from the list of goals.
36: */
37: void proofGoalRemoved(ProofTreeEvent e);
38:
39: /** The goals mentiones in the list of added goals in the proof
40: * event have been added to the proof
41: */
42: void proofGoalsAdded(ProofTreeEvent e);
43:
44: /**
45: * The goals mentiones in the list of added goals in the proof
46: * event have been added to the proof
47: */
48: void proofGoalsChanged(ProofTreeEvent e);
49:
50: }
|