001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.proof.proofevent;
012:
013: import de.uka.ilkd.key.logic.SequentChangeInfo;
014: import de.uka.ilkd.key.proof.*;
015: import de.uka.ilkd.key.rule.RuleApp;
016:
017: /**
018: * Collect changes applied to a node during a given period of time
019: */
020: public class NodeChangeJournal implements GoalListener {
021:
022: private final Proof proof;
023:
024: /**
025: * The original node
026: */
027: private final Node node;
028:
029: /**
030: * This is a may storing the leaves that are currently below
031: * the original node, and all changes applied to each of them
032: */
033: private MapFromNodeToNodeChangesHolder changes = MapAsListFromNodeToNodeChangesHolder.EMPTY_MAP;
034:
035: /**
036: * @param p_goal the original goal/node
037: */
038: public NodeChangeJournal(Proof p_proof, Goal p_goal) {
039: proof = p_proof;
040: node = p_goal.node();
041: putChangeObj(node, new NodeChangesHolder());
042: }
043:
044: /**
045: * Create an RuleAppInfo object containing all changes stored
046: * within this object; remove all listeners
047: */
048: public RuleAppInfo getRuleAppInfo(RuleApp p_ruleApp) {
049: IteratorOfEntryOfNodeAndNodeChangesHolder it = changeObjIterator();
050: ListOfNodeReplacement nrs = SLListOfNodeReplacement.EMPTY_LIST;
051:
052: while (it.hasNext()) {
053: final EntryOfNodeAndNodeChangesHolder entry = it.next();
054: final Node newNode = entry.key();
055: final Goal newGoal = proof.getGoal(newNode);
056:
057: if (newGoal != null) {
058: final NodeChangesHolder nc = entry.value();
059:
060: nrs = nrs.prepend(new NodeReplacement(newNode, node,
061: nc.scis));
062:
063: newGoal.removeGoalListener(this );
064: }
065: }
066:
067: return new RuleAppInfo(p_ruleApp, node, nrs);
068: }
069:
070: // GoalListener methods
071:
072: /**
073: * informs the listener about a change that occured to the sequent
074: * of goal
075: */
076: public void sequentChanged(Goal source, SequentChangeInfo sci) {
077: NodeChangesHolder nc = getChangeObj(source.node());
078:
079: if (nc != null)
080: nc.addSCI(sci);
081: }
082:
083: /**
084: * Informs the listener that the given goal <code>source</code>
085: * has been replaced by the goals <code>newGoals</code> (note that
086: * <code>source</code> may be an element of
087: * <code>newGoals</code>). The nodes of <code>newGoals</code> are
088: * children of the node <code>parent</code>
089: */
090: public void goalReplaced(Goal source, Node parent,
091: ListOfGoal newGoals) {
092: NodeChangesHolder nc = removeChangeObj(parent);
093:
094: if (nc != null) {
095: IteratorOfGoal it = newGoals.iterator();
096: if (it.hasNext()) {
097: while (true) {
098: putChangeObj(it.next().node(), nc);
099: if (!it.hasNext())
100: break;
101: nc = (NodeChangesHolder) nc.clone();
102: }
103: }
104: }
105: }
106:
107: private void putChangeObj(Node p_node, NodeChangesHolder p_obj) {
108: changes = changes.put(p_node, p_obj);
109: }
110:
111: private NodeChangesHolder getChangeObj(Node p_node) {
112: return changes.get(p_node);
113: }
114:
115: private NodeChangesHolder removeChangeObj(Node p_node) {
116: final NodeChangesHolder res = changes.get(p_node);
117: changes = changes.remove(p_node);
118: return res;
119: }
120:
121: private IteratorOfEntryOfNodeAndNodeChangesHolder changeObjIterator() {
122: return changes.entryIterator();
123: }
124:
125: }
|