Fixed Scala_Isabelle_Master_Control_Program.thy to work with Isabelle…

… <=2021.
dominique-unruh · Jul 8, 2024 · ee5158b · ee5158b
1 parent 7d355d1
commit ee5158b
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/src/main/resources/de/unruh/isabelle/control/Scala_Isabelle_Master_Control_Program.thy b/src/main/resources/de/unruh/isabelle/control/Scala_Isabelle_Master_Control_Program.thy
@@ -8,8 +8,9 @@ ML \<open>
 fun run_one_of_these_ml mls = let
   val errors = Unsynchronized.ref []
   fun run_single ml = 
-    Context.>> (Local_Theory.touch_ml_env #> ML_Context.exec (fn () =>
-                ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) ml) #>
+    Context.>> ((* Local_Theory.touch_ml_env #> (* Does not exist in Isabelle \<le>2021 *) *)
+                ML_Context.exec (fn () =>
+                  ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) ml) #>
                 Local_Theory.propagate_ml_env)
   fun run [] = raise ERROR ("Could not run any of the ML codes. Errors were:\n" ^
                             String.concatWith "\n" (!errors))