de.uka.ilkd.key.proof

Class ProofTreeAdapter

java.lang.Object

de.uka.ilkd.key.proof.ProofTreeAdapter

All Implemented Interfaces:

ProofTreeListener

Direct Known Subclasses:

DefaultGoalChooser.ProofTreeObserver, GUIProofTreeModel.ProofTreeListener, KeYMediator.KeYMediatorProofTreeListener, ProofCorrectnessMgt.DefaultMgtProofTreeListener, TaskTree.TaskTreeProofTreeListener

public abstract class ProofTreeAdapter
extends java.lang.Object
implements ProofTreeListener

An abstract adapter class for receiving proof tree events. proofStructureChanged has an empty implementation, the other methods delegate to proofStructureChanged.

Extend this class to create a ProofTreeEvent listener and override the implementation of proofStructureChanged to provide a simple reaction to any kind of event, or also override the other methods to provide more fine-grained actions.

Constructor Summary

Constructors

Constructor and Description
ProofTreeAdapter()

Method Summary

Modifier and Type	Method and Description
void	notesChanged(ProofTreeEvent e) If the notes of a NodeInfo of a proof tree Node have changed.
void	proofClosed(ProofTreeEvent e) The proof trees has been closed (the list of goals is empty).
void	proofExpanded(ProofTreeEvent e) The node mentioned in the ProofTreeEvent has changed, and/or there are new descendants of that node.
void	proofGoalRemoved(ProofTreeEvent e) The goal mentioned in the ProofTreeEvent has been removed from the list of goals.
void	proofGoalsAdded(ProofTreeEvent e) The goals mentiones in the list of added goals in the proof event have been added to the proof
void	proofGoalsChanged(ProofTreeEvent e) The goals mentiones in the list of added goals in the proof event have been added to the proof
void	proofIsBeingPruned(ProofTreeEvent e) The proof tree under the node mentioned in the ProofTreeEvent is in pruning phase.
void	proofPruned(ProofTreeEvent e) The proof tree has been pruned under the node mentioned in the ProofTreeEvent.
void	proofStructureChanged(ProofTreeEvent e) The structure of the proof has changed radically.
void	smtDataUpdate(ProofTreeEvent e) If, e.g., an SMT Solver was applied to node/goal referenced in e, then this event occurs in order to monitor, e.g. by a dialog, the result of the SMT solver.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

ProofTreeAdapter

public ProofTreeAdapter()

Method Detail

proofExpanded

public void proofExpanded(ProofTreeEvent e)

The node mentioned in the ProofTreeEvent has changed, and/or there are new descendants of that node. Any nodes that are not descendants of that node are unaffected.

Specified by:

proofExpanded in interface ProofTreeListener

proofIsBeingPruned

public void proofIsBeingPruned(ProofTreeEvent e)

The proof tree under the node mentioned in the ProofTreeEvent is in pruning phase. The subtree of node will be removed after this call but at this point the subtree can still be traversed (e.g. in order to free the nodes in caches). The method proofPruned is called, when the nodes are disconnect from node.

Specified by:

proofIsBeingPruned in interface ProofTreeListener

proofPruned

public void proofPruned(ProofTreeEvent e)

The proof tree has been pruned under the node mentioned in the ProofTreeEvent. In other words, that node should no longer have any children now. Any nodes that were not descendants of that node are unaffected.

Specified by:

proofPruned in interface ProofTreeListener

proofStructureChanged

public void proofStructureChanged(ProofTreeEvent e)

The structure of the proof has changed radically. Any client should rescan the whole proof tree.

Specified by:

proofStructureChanged in interface ProofTreeListener

proofClosed

public void proofClosed(ProofTreeEvent e)

The proof trees has been closed (the list of goals is empty).

Specified by:

proofClosed in interface ProofTreeListener

proofGoalRemoved

public void proofGoalRemoved(ProofTreeEvent e)

The goal mentioned in the ProofTreeEvent has been removed from the list of goals.

Specified by:

proofGoalRemoved in interface ProofTreeListener

proofGoalsAdded

public void proofGoalsAdded(ProofTreeEvent e)

The goals mentiones in the list of added goals in the proof event have been added to the proof

Specified by:

proofGoalsAdded in interface ProofTreeListener

proofGoalsChanged

public void proofGoalsChanged(ProofTreeEvent e)

The goals mentiones in the list of added goals in the proof event have been added to the proof

Specified by:

proofGoalsChanged in interface ProofTreeListener

smtDataUpdate

public void smtDataUpdate(ProofTreeEvent e)

If, e.g., an SMT Solver was applied to node/goal referenced in e, then this event occurs in order to monitor, e.g. by a dialog, the result of the SMT solver. The data from the SMT solver can be accessed via. Node.getCounterExData()

Specified by:

smtDataUpdate in interface ProofTreeListener

notesChanged

public void notesChanged(ProofTreeEvent e)

If the notes of a NodeInfo of a proof tree Node have changed.

Specified by:

notesChanged in interface ProofTreeListener

Parameters:

e - The ProofTreeEvent.