Fixed startup code to work with Isabelle2024.

src/main/resources/de/unruh/isabelle/control/Scala_Isabelle_Master_Control_Program.thy

@@ -2,14 +2,47 @@ theory Scala_Isabelle_Master_Control_Program
   imports Pure
 begin
 
+(* run_one_of_these_ml will try to compile and execute all the given ML fragments
+    until one of them successfully compiles and executes. *)
+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) #>
+                Local_Theory.propagate_ml_env)
+  fun run [] = raise ERROR ("Could not run any of the ML codes. Errors were:\n" ^
+                            String.concatWith "\n" (!errors))
+    | run (ml::mls) = run_single ml
+                      handle ERROR e => (errors := e :: !errors; run mls)
+in
+  run mls
+end
+\<close>
+
+(* Define compatibility aliases for Mutex.mutex and friends.
+   For use in control_isabelle.ml only *)
+ML \<open>
+run_one_of_these_ml [
+  \<open>type mcp_mutex = Mutex.mutex val mcp_mutex = Mutex.mutex val mcp_mutex_lock = Mutex.lock val mcp_mutex_unlock = Mutex.unlock\<close>,
+  \<open>type mcp_mutex = Thread.Mutex.mutex val mcp_mutex = Thread.Mutex.mutex val mcp_mutex_lock = Thread.Mutex.lock val mcp_mutex_unlock = Thread.Mutex.unlock\<close>]
+\<close>
+
+(* Do the equivalent of `declare [[ML_catch_all = true]]`, but without error if it fails *)
+ML \<open>
+run_one_of_these_ml [\<open>Context.>> (Context.map_theory (Config.put_global ML_Compiler.ML_catch_all true))\<close>,
+                     \<open>\<close>]
+\<close>
+
+
 ML_file "control_isabelle.ml"
 
 ML \<open>
 let
 val path = File.platform_path (Path.explode "WORKING_DIRECTORY")
 in
   OS.FileSys.chDir path
-  handle OS.SysErr (msg,_) => error ("Could set Isabelle working directory as " ^ path ^ ": " ^ msg)
+  handle OS.SysErr (msg,_) => error ("Could not set Isabelle working directory as " ^ path ^ ": " ^ msg)
 end
 \<close>
 

src/main/resources/de/unruh/isabelle/control/control_isabelle.ml

@@ -26,7 +26,7 @@ structure Control_Isabelle : sig
   exception E_ToplevelState of Toplevel.state
   exception E_Transition of Toplevel.transition  
   exception E_Keywords of Thy_Header.keywords
-  exception E_Mutex of Mutex.mutex
+  exception E_Mutex of mcp_mutex
   exception E_Proofterm of Proofterm.proof
   exception E_Data of data
 
@@ -62,7 +62,7 @@ exception E_Position of Position.T
 exception E_ToplevelState of Toplevel.state
 exception E_Transition of Toplevel.transition
 exception E_Keywords of Thy_Header.keywords
-exception E_Mutex of Mutex.mutex
+exception E_Mutex of mcp_mutex
 exception E_Proofterm of Proofterm.proof
 exception E_Data of data
 
@@ -75,11 +75,11 @@ val (inSecret, outSecret) = SECRETS
 (* val outStream = BinIO.openOut outputPipeName *)
 
 (* Any sending of data, and any adding of data to the object store must use this mutex *)
-val mutex = Mutex.mutex ()
+val mutex = mcp_mutex ()
 fun withMutex f x = let
-  val _ = Mutex.lock mutex
-  val result = f x handle e => (Mutex.unlock mutex; Exn.reraise e)
-  val _ = Mutex.unlock mutex
+  val _ = mcp_mutex_lock mutex
+  val result = f x handle e => (mcp_mutex_unlock mutex; Exn.reraise e)
+  val _ = mcp_mutex_unlock mutex
 in result end
 
 val objectsMax = Unsynchronized.ref 0
@@ -260,12 +260,12 @@ fun runAsync seq f =
 (* Context for compiling ML code in. Can be mutated when declaring new ML symbols *)
 val ml_compilation_context = Unsynchronized.ref (Context.Theory \<^theory>)
 (* Mutex for updating the context above *)
-val ml_compilation_mutex = Mutex.mutex ()
+val ml_compilation_mutex = mcp_mutex ()
 fun update_ml_compilation_context f = let
-  val _ = Mutex.lock ml_compilation_mutex
+  val _ = mcp_mutex_lock ml_compilation_mutex
   val _ = (ml_compilation_context := f (!ml_compilation_context))
-             handle e => (Mutex.unlock ml_compilation_mutex; Exn.reraise e)
-  val _ = Mutex.unlock ml_compilation_mutex
+             handle e => (mcp_mutex_unlock ml_compilation_mutex; Exn.reraise e)
+  val _ = mcp_mutex_unlock ml_compilation_mutex
   in () end
 (* Executes ML code in the namespace of context, and updates that namespace (side effect) *)
 fun executeML_update (ml:string) = let

src/main/resources/de/unruh/isabelle/control/control_isabelle_logged.ml

@@ -37,7 +37,7 @@ structure Control_Isabelle : sig
   exception E_ToplevelState of Toplevel.state
   exception E_Transition of Toplevel.transition
   exception E_Keywords of Thy_Header.keywords
-  exception E_Mutex of Mutex.mutex
+  exception E_Mutex of mcp_mutex
   exception E_Proofterm of Proofterm.proof
   exception E_Data of data
 
@@ -74,7 +74,7 @@ exception E_Position of Position.T
 exception E_ToplevelState of Toplevel.state
 exception E_Transition of Toplevel.transition
 exception E_Keywords of Thy_Header.keywords
-exception E_Mutex of Mutex.mutex
+exception E_Mutex of mcp_mutex
 exception E_Proofterm of Proofterm.proof
 exception E_Data of data
 
@@ -174,11 +174,11 @@ fun logSendReplyData seq data =
 (* val outStream = BinIO.openOut outputPipeName *)
 
 (* Any sending of data, and any adding of data to the object store must use this mutex *)
-val mutex = Mutex.mutex ()
+val mutex = mcp_mutex ()
 fun withMutex f x = let
-  val _ = Mutex.lock mutex
-  val result = f x handle e => (Mutex.unlock mutex; Exn.reraise e)
-  val _ = Mutex.unlock mutex
+  val _ = mcp_mutex_lock mutex
+  val result = f x handle e => (mcp_mutex_unlock mutex; Exn.reraise e)
+  val _ = mcp_mutex_unlock mutex
 in result end
 
 val objectsMax = Unsynchronized.ref 0
@@ -373,12 +373,12 @@ fun runAsync seq f =
 (* Context for compiling ML code in. Can be mutated when declaring new ML symbols *)
 val ml_compilation_context = Unsynchronized.ref (Context.Theory \<^theory>)
 (* Mutex for updating the context above *)
-val ml_compilation_mutex = Mutex.mutex ()
+val ml_compilation_mutex = mcp_mutex ()
 fun update_ml_compilation_context f = let
-  val _ = Mutex.lock ml_compilation_mutex
+  val _ = mcp_mutex_lock ml_compilation_mutex
   val _ = (ml_compilation_context := f (!ml_compilation_context))
-             handle e => (Mutex.unlock ml_compilation_mutex; Exn.reraise e)
-  val _ = Mutex.unlock ml_compilation_mutex
+             handle e => (mcp_mutex_unlock ml_compilation_mutex; Exn.reraise e)
+  val _ = mcp_mutex_unlock ml_compilation_mutex
   in () end
 (* Executes ML code in the namespace of context, and updates that namespace (side effect) *)
 fun executeML_update (ml:string) = let