de.uka.ilkd.key.proof.proofevent

Class NodeChangeJournal

java.lang.Object

de.uka.ilkd.key.proof.proofevent.NodeChangeJournal

All Implemented Interfaces:

GoalListener

public class NodeChangeJournal
extends java.lang.Object
implements GoalListener

Collect changes applied to a node during a given period of time

Field Summary

Fields

Modifier and Type	Field and Description
private ImmutableMap<Node,NodeChangesHolder>	changes This is a may storing the leaves that are currently below the original node, and all changes applied to each of them
private Node	node The original node
private Proof	proof

Constructor Summary

Constructors

Constructor and Description
NodeChangeJournal(Proof p_proof, Goal p_goal)

Method Summary

Modifier and Type	Method and Description
void	automaticStateChanged(Goal source, boolean oldAutomatic, boolean newAutomatic) Informs the listener that the automatic state Goal.isAutomatic() has changed.
private NodeChangesHolder	getChangeObj(Node p_node)
RuleAppInfo	getRuleAppInfo(RuleApp p_ruleApp) Create an RuleAppInfo object containing all changes stored within this object; remove all listeners
void	goalReplaced(Goal source, Node parent, ImmutableList<Goal> newGoals) Informs the listener that the given goal source has been replaced by the goals newGoals (note that source may be an element of newGoals).
private void	putChangeObj(Node p_node, NodeChangesHolder p_obj)
private NodeChangesHolder	removeChangeObj(Node p_node)
void	sequentChanged(Goal source, SequentChangeInfo sci) informs the listener about a change that occured to the sequent of goal

Methods inherited from class java.lang.Object

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

Field Detail

proof

private final Proof proof

node

private final Node node

The original node

changes

private ImmutableMap<Node,NodeChangesHolder> changes

This is a may storing the leaves that are currently below the original node, and all changes applied to each of them

Constructor Detail

NodeChangeJournal

public NodeChangeJournal(Proof p_proof,
                         Goal p_goal)

Parameters:

p_goal - the original goal/node

Method Detail

getRuleAppInfo

public RuleAppInfo getRuleAppInfo(RuleApp p_ruleApp)

Create an RuleAppInfo object containing all changes stored within this object; remove all listeners

sequentChanged

public void sequentChanged(Goal source,
                           SequentChangeInfo sci)

informs the listener about a change that occured to the sequent of goal

Specified by:

sequentChanged in interface GoalListener

goalReplaced

public void goalReplaced(Goal source,
                         Node parent,
                         ImmutableList<Goal> newGoals)

Informs the listener that the given goal source has been replaced by the goals newGoals (note that source may be an element of newGoals). The nodes of newGoals are children of the node parent

Specified by:

goalReplaced in interface GoalListener

putChangeObj

private void putChangeObj(Node p_node,
                          NodeChangesHolder p_obj)

getChangeObj

private NodeChangesHolder getChangeObj(Node p_node)

removeChangeObj

private NodeChangesHolder removeChangeObj(Node p_node)

automaticStateChanged

public void automaticStateChanged(Goal source,
                                  boolean oldAutomatic,
                                  boolean newAutomatic)

Description copied from interface: GoalListener

Informs the listener that the automatic state Goal.isAutomatic() has changed.

Specified by:

automaticStateChanged in interface GoalListener

Parameters:

source - The changed Goal.

oldAutomatic - The old state.

newAutomatic - The new state.