Fixed pure.Mutex.scala.

(Uses Thread.Mutex.mutex etc. from Isabelle2024 on.)

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

@@ -37,6 +37,7 @@ structure Control_Isabelle : sig
   val message_of_exn : Proof.context option -> exn -> string
   val string_of_data : data -> string
   val sendToScala : data -> unit
+  type mutex = mcp_mutex
 end
 =
 struct
@@ -355,4 +356,7 @@ fun handleLines () = (checkSecret (); handleLines' 0)
 
 val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF)
 
+(* This provides a name for Thread.Mutex.mutex / Mutex.mutex that is independent of the Isabelle version *)
+type mutex = mcp_mutex
+
 end

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

@@ -48,6 +48,7 @@ structure Control_Isabelle : sig
   val message_of_exn : Proof.context option -> exn -> string
   val string_of_data : data -> string
   val sendToScala : data -> unit
+  type mutex = mcp_mutex
 end
 =
 struct
@@ -462,4 +463,7 @@ fun handleLines () = (checkSecret (); handleLines' 0)
 
 val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF)
 
+(* This provides a name for Thread.Mutex.mutex / Mutex.mutex that is independent of the Isabelle version *)
+type mutex = mcp_mutex
+
 end

src/main/scala/de/unruh/isabelle/mlvalue/Version.scala

@@ -130,5 +130,10 @@ object Version extends OperationCollection {
    * Unspecified behavior on development versions. */
   def from2023(implicit isabelle: Isabelle): Boolean = year >= 2023
 
+  /** True, if the current version is at least Isabelle2024 (including the release candidates).
+   *
+   * Unspecified behavior on development versions. */
+  def from2024(implicit isabelle: Isabelle): Boolean = year >= 2024
+
   private val logger = log4s.getLogger
 }

src/main/scala/de/unruh/isabelle/pure/Mutex.scala

@@ -1,10 +1,10 @@
 package de.unruh.isabelle.pure
 
 import de.unruh.isabelle.control.Isabelle
-import de.unruh.isabelle.mlvalue.{MLValue, MLValueWrapper}
+import de.unruh.isabelle.mlvalue.{MLValue, MLValueWrapper, Version}
 import de.unruh.isabelle.mlvalue.MLValue.{compileFunction, compileFunction0, compileValue}
 
-/** Represents a mutex (ML type `Mutex.mutex`) in the Isabelle process.
+/** Represents a mutex (ML type `Thread.Mutex.mutex`) in the Isabelle process.
  *
  * An instance of this class is merely a thin wrapper around an [[mlvalue.MLValue MLValue]],
  * all explanations and examples given for [[Context]] also apply here.
@@ -17,16 +17,20 @@ final class Mutex private [Mutex](val mlValue : MLValue[Mutex]) extends MLValueW
 }
 
 object Mutex extends MLValueWrapper.Companion[Mutex] {
-  override protected val mlType = "Mutex.mutex"
+  /** This is equivalent to `Thread.Mutex.mutex` or `Mutex.mutex`, depending on the Isabelle version. */
+  override lazy protected val mlType = "Control_Isabelle.mutex"
   override protected val predefinedException: String = "E_Mutex"
 
   override protected def instantiate(mlValue: MLValue[Mutex]): Mutex = new Mutex(mlValue)
 
   //noinspection TypeAnnotation
   protected class Ops(implicit isabelle: Isabelle) extends super.Ops {
-    lazy val createMutex = compileFunction0[Mutex]("Mutex.mutex")
+    lazy val createMutex = compileFunction0[Mutex](s"$mutexStruct.mutex")
   }
 
+  private def mutexStruct(implicit isabelle: Isabelle) =
+    if (Version.from2024) "Thread.Mutex" else "Mutex"
+
   /** Creates a new mutex */
   def apply()(implicit isabelle: Isabelle) : Mutex = Ops.createMutex().retrieveNow
 
@@ -44,8 +48,8 @@ object Mutex extends MLValueWrapper.Companion[Mutex] {
    * `Thy_Info.use_thy` is not thread safe. (In practice, better use [[Theory.mutex]] as the mutex instead
    * of your own in this specific case.)
    **/
-  def wrapWithMutex(mutex: String, code: String) =
-    s"let val _ = Mutex.lock $mutex val result = ($code) handle e => (Mutex.unlock $mutex; Exn.reraise e) val _ = Mutex.unlock $mutex in result end"
+  def wrapWithMutex(mutex: String, code: String)(implicit isabelle: Isabelle) =
+    s"let val _ = $mutexStruct.lock $mutex val result = ($code) handle e => ($mutexStruct.unlock $mutex; Exn.reraise e) val _ = $mutexStruct.unlock $mutex in result end"
 
   override protected def newOps(implicit isabelle: Isabelle): Ops = new Ops
 }