From ee5158b72d87dbdcc97ad800f9f5ed36bd6d320e Mon Sep 17 00:00:00 2001 From: Dominique Unruh Date: Mon, 8 Jul 2024 17:22:25 +0200 Subject: [PATCH] Fixed Scala_Isabelle_Master_Control_Program.thy to work with Isabelle <=2021. --- .../control/Scala_Isabelle_Master_Control_Program.thy | 5 +++-- 1 file changed, 3 insertions(+), 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 index 34775b2..56ff73f 100644 --- 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 \ 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 \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))