Fully disable origin tracking if it is disabled

Related KeYProject#3253
FliegendeWurst · Sep 5, 2023 · afcdf6f · afcdf6f
1 parent f85a298
commit afcdf6f
Show file tree

Hide file tree

Showing 2 changed files with 22 additions and 1 deletion.
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/Services.java b/key.core/src/main/java/de/uka/ilkd/key/java/Services.java
@@ -14,6 +14,7 @@
 import de.uka.ilkd.key.proof.init.InitConfig;
 import de.uka.ilkd.key.proof.init.Profile;
 import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
+import de.uka.ilkd.key.settings.ProofIndependentSettings;
 import de.uka.ilkd.key.util.Debug;
 import de.uka.ilkd.key.util.KeYRecoderExcHandler;
 
@@ -298,6 +299,10 @@ public void setProof(Proof p_proof) {
                 "Services are already owned by another proof:" + proof.name());
         }
         proof = p_proof;
+        if (!ProofIndependentSettings.DEFAULT_INSTANCE.getTermLabelSettings().getUseOriginLabels()
+                || !proof.getSettings().getTermLabelSettings().getUseOriginLabels()) {
+            profile.getTermLabelManager().disableOriginLabelRefactorings();
+        }
     }
 
 

diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelManager.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelManager.java
@@ -5,6 +5,7 @@
 
 import java.util.*;
 import java.util.Map.Entry;
+import java.util.Set;
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.*;
@@ -15,8 +16,13 @@
 import de.uka.ilkd.key.proof.init.Profile;
 import de.uka.ilkd.key.rule.Rule;
 import de.uka.ilkd.key.rule.RuleApp;
-import de.uka.ilkd.key.rule.label.*;
+import de.uka.ilkd.key.rule.label.ChildTermLabelPolicy;
+import de.uka.ilkd.key.rule.label.OriginTermLabelRefactoring;
+import de.uka.ilkd.key.rule.label.TermLabelMerger;
+import de.uka.ilkd.key.rule.label.TermLabelPolicy;
+import de.uka.ilkd.key.rule.label.TermLabelRefactoring;
 import de.uka.ilkd.key.rule.label.TermLabelRefactoring.RefactoringScope;
+import de.uka.ilkd.key.rule.label.TermLabelUpdate;
 import de.uka.ilkd.key.util.LinkedHashMap;
 import de.uka.ilkd.key.util.Pair;
 
@@ -2194,4 +2200,14 @@ protected void mergeLabels(SequentChangeInfo currentSequent, Services services,
             }
         }
     }
+
+    /**
+     * Fully disable origin tracking. This will remove the {@link OriginTermLabelRefactoring} from
+     * the manager.
+     */
+    public void disableOriginLabelRefactorings() {
+        allRulesRefactorings = ImmutableList.fromList(
+            allRulesRefactorings.stream().filter(x -> !(x instanceof OriginTermLabelRefactoring))
+                    .toList());
+    }
 }