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: package de.uka.ilkd.key.strategy.feature;
09:
10: import de.uka.ilkd.key.logic.PosInOccurrence;
11: import de.uka.ilkd.key.proof.Goal;
12: import de.uka.ilkd.key.proof.Node;
13: import de.uka.ilkd.key.proof.NodeInfo;
14: import de.uka.ilkd.key.rule.RuleApp;
15: import de.uka.ilkd.key.visualdebugger.HashMapFromPosInOccurrenceToLabel;
16: import de.uka.ilkd.key.visualdebugger.PCLabel;
17:
18: public class LabelFeature extends BinaryFeature {
19:
20: public static final LabelFeature INSTANCE = new LabelFeature();
21:
22: private LabelFeature() {
23: }
24:
25: protected boolean filter(RuleApp app, PosInOccurrence pos, Goal goal) {
26: if (goal.node().root())
27: return false;
28:
29: final Node parent = goal.node().parent();
30: final RuleApp previouslyAppliedRuleApp = parent
31: .getAppliedRuleApp();
32: if (previouslyAppliedRuleApp.posInOccurrence() == null)
33: return false;
34:
35: final PosInOccurrence pio = previouslyAppliedRuleApp
36: .posInOccurrence().topLevel();
37:
38: final NodeInfo nodeInfo = parent.getNodeInfo();
39: final HashMapFromPosInOccurrenceToLabel debugLabels = nodeInfo
40: .getVisualDebuggerState().getLabels();
41:
42: if (debugLabels.containsKey(pio)) {
43: if (((PCLabel) debugLabels.get(pio)).isLooking()) {
44: return true;
45: }
46: if (nodeInfo.getActiveStatement() != null) {
47: return true; //TODO act statement in prog mod
48: }
49: }
50:
51: return false;
52: }
53: }
|