de.uka.ilkd.key.gui

Class GoalList.GoalListModel.GoalListProofTreeListener

java.lang.Object

de.uka.ilkd.key.gui.GoalList.GoalListModel.GoalListProofTreeListener

All Implemented Interfaces:

ProofTreeListener, java.io.Serializable

Enclosing class:

GoalList.GoalListModel

class GoalList.GoalListModel.GoalListProofTreeListener
extends java.lang.Object
implements ProofTreeListener, java.io.Serializable

Field Summary

Fields

Modifier and Type	Field and Description
private boolean	pruningInProcess
private static long	serialVersionUID

Constructor Summary

Constructors

Constructor and Description
GoalListProofTreeListener()

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) invoked if all goals of the proof are closed
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) invoked if the list of goals changed (goals were added, removed etc.
void	proofGoalsAdded(ProofTreeEvent e) invoked if the current goal of the proof changed
void	proofGoalsChanged(ProofTreeEvent e) invoked if the current goal of the proof changed
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

Field Detail

serialVersionUID

private static final long serialVersionUID

See Also:

Constant Field Values

pruningInProcess

private boolean pruningInProcess

Constructor Detail

GoalListProofTreeListener

GoalListProofTreeListener()

Method Detail

proofExpanded

public void proofExpanded(ProofTreeEvent e)

Description copied from interface: ProofTreeListener

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

proofClosed

public void proofClosed(ProofTreeEvent e)

invoked if all goals of the proof are closed

Specified by:

proofClosed in interface ProofTreeListener

proofIsBeingPruned

public void proofIsBeingPruned(ProofTreeEvent e)

Description copied from interface: ProofTreeListener

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

proofGoalRemoved

public void proofGoalRemoved(ProofTreeEvent e)

invoked if the list of goals changed (goals were added, removed etc.

Specified by:

proofGoalRemoved in interface ProofTreeListener

proofGoalsAdded

public void proofGoalsAdded(ProofTreeEvent e)

invoked if the current goal of the proof changed

Specified by:

proofGoalsAdded in interface ProofTreeListener

proofGoalsChanged

public void proofGoalsChanged(ProofTreeEvent e)

invoked if the current goal of the proof changed

Specified by:

proofGoalsChanged in interface ProofTreeListener

proofStructureChanged

public void proofStructureChanged(ProofTreeEvent e)

Description copied from interface: ProofTreeListener

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

Specified by:

proofStructureChanged in interface ProofTreeListener

smtDataUpdate

public void smtDataUpdate(ProofTreeEvent e)

Description copied from interface: ProofTreeListener

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)

Description copied from interface: ProofTreeListener

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

Specified by:

notesChanged in interface ProofTreeListener

Parameters:

e - The ProofTreeEvent.