allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;

--- a/NEWS	Tue Sep 29 12:12:34 2020 +0200
+++ b/NEWS	Tue Sep 29 13:19:34 2020 +0200
@@ -159,9 +159,9 @@
 Theory.join_theory from Isabelle2020). Special extend/merge behaviour at
 the begin of a new theory can be achieved via Theory.at_begin.
 
-* Antiquotations @{scala_function} and @{scala} refer to registered
-Isabelle/Scala functions (of type String => String): invocation works
-via the PIDE protocol.
+* Antiquotations @{scala_function}, @{scala}, @{scala_thread} refer to
+registered Isabelle/Scala functions (of type String => String):
+invocation works via the PIDE protocol.
 
 
 *** System ***

--- a/etc/symbols	Tue Sep 29 12:12:34 2020 +0200
+++ b/etc/symbols	Tue Sep 29 13:19:34 2020 +0200
@@ -422,6 +422,7 @@
 \<^scala_function>      argument: cartouche
 \<^scala_method>        argument: cartouche
 \<^scala_object>        argument: cartouche
+\<^scala_thread>        argument: cartouche
 \<^scala_type>          argument: cartouche
 \<^session>             argument: cartouche
 \<^simproc>             argument: cartouche

--- a/src/Doc/System/Scala.thy	Tue Sep 29 12:12:34 2020 +0200
+++ b/src/Doc/System/Scala.thy	Tue Sep 29 13:19:34 2020 +0200
@@ -210,21 +210,25 @@
   \begin{matharray}{rcl}
   @{ML_antiquotation_def "scala_function"} & : & \<open>ML_antiquotation\<close> \\
   @{ML_antiquotation_def "scala"} & : & \<open>ML_antiquotation\<close> \\
+  @{ML_antiquotation_def "scala_thread"} & : & \<open>ML_antiquotation\<close> \\
   \end{matharray}
 
   \<^rail>\<open>
-    (@{ML_antiquotation scala_function} | @{ML_antiquotation scala})
-      @{syntax embedded}
+    (@{ML_antiquotation scala_function} |
+     @{ML_antiquotation scala} |
+     @{ML_antiquotation scala_thread}) @{syntax embedded}
   \<close>
 
   \<^descr> \<open>@{scala_function name}\<close> inlines the checked function name as ML string
     literal.
 
-  \<^descr> \<open>@{scala name}\<close> invokes the checked function via the PIDE protocol. In
-  Isabelle/ML this appears as a function of type
+  \<^descr> \<open>@{scala name}\<close> and \<open>@{scala_thread name}\<close> invoke the checked function via
+  the PIDE protocol. In Isabelle/ML this appears as a function of type
   \<^ML_type>\<open>string -> string\<close>, which is subject to interrupts within the ML
   runtime environment as usual. A \<^scala>\<open>null\<close> result in Scala raises an
-  exception \<^ML>\<open>Scala.Null\<close> in ML.
+  exception \<^ML>\<open>Scala.Null\<close> in ML. The execution of \<open>@{scala}\<close> works via a
+  Scala future on a bounded thread farm, while \<open>@{scala_thread}\<close> always forks
+  a separate Java thread.
 
   The standard approach of representing datatypes via strings works via XML in
   YXML transfer syntax. See Isabelle/ML operations and modules @{ML

--- a/src/Pure/PIDE/markup.ML	Tue Sep 29 12:12:34 2020 +0200
+++ b/src/Pure/PIDE/markup.ML	Tue Sep 29 13:19:34 2020 +0200
@@ -213,7 +213,7 @@
   val commands_accepted: Properties.T
   val assign_update: Properties.T
   val removed_versions: Properties.T
-  val invoke_scala: string -> string -> Properties.T
+  val invoke_scala: string -> string -> bool -> Properties.T
   val cancel_scala: string -> Properties.T
   val task_statistics: Properties.entry
   val command_timing: Properties.entry
@@ -679,7 +679,9 @@
 val assign_update = [(functionN, "assign_update")];
 val removed_versions = [(functionN, "removed_versions")];
 
-fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
+fun invoke_scala name id thread =
+  [(functionN, "invoke_scala"), (nameN, name), (idN, id), ("thread", Value.print_bool thread)];
+
 fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
 
 val task_statistics = (functionN, "task_statistics");

--- a/src/Pure/PIDE/markup.scala	Tue Sep 29 12:12:34 2020 +0200
+++ b/src/Pure/PIDE/markup.scala	Tue Sep 29 13:19:34 2020 +0200
@@ -605,9 +605,10 @@
 
   object Invoke_Scala extends Function("invoke_scala")
   {
-    def unapply(props: Properties.T): Option[(String, String)] =
+    def unapply(props: Properties.T): Option[(String, String, Boolean)] =
       props match {
-        case List(PROPERTY, (NAME, name), (ID, id)) => Some((name, id))
+        case List(PROPERTY, (NAME, name), (ID, id), ("thread", Value.Boolean(thread))) =>
+          Some((name, id, thread))
         case _ => None
       }
   }

--- a/src/Pure/System/scala.ML	Tue Sep 29 12:12:34 2020 +0200
+++ b/src/Pure/System/scala.ML	Tue Sep 29 13:19:34 2020 +0200
@@ -8,6 +8,7 @@
 sig
   exception Null
   val function: string -> string -> string
+  val function_thread: string -> string -> string
   val functions: unit -> string list
   val check_function: Proof.context -> string * Position.T -> string
 end;
@@ -40,15 +41,13 @@
           | _ => raise Fail ("Bad tag: " ^ tag));
       in Synchronized.change results (Symtab.map_entry id (K result)) end);
 
-in
-
-fun function name arg =
+fun gen_function thread name arg =
   Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
     let
       val id = new_id ();
       fun invoke () =
        (Synchronized.change results (Symtab.update (id, Exn.Exn Match));
-        Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg]);
+        Output.protocol_message (Markup.invoke_scala name id thread) [XML.Text arg]);
       fun cancel () =
        (Synchronized.change results (Symtab.delete_safe id);
         Output.protocol_message (Markup.cancel_scala id) []);
@@ -65,6 +64,11 @@
       Exn.release (restore_attributes await_result ())
     end) ();
 
+in
+
+val function = gen_function false;
+val function_thread = gen_function true;
+
 end;
 
 
@@ -84,6 +88,10 @@
   ML_Antiquotation.value_embedded \<^binding>\<open>scala\<close>
     (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) =>
       let val name = check_function ctxt arg
-      in ML_Syntax.atomic ("Scala.function " ^ ML_Syntax.print_string name) end)));
+      in ML_Syntax.atomic ("Scala.function " ^ ML_Syntax.print_string name) end)) #>
+  ML_Antiquotation.value_embedded \<^binding>\<open>scala_thread\<close>
+    (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) =>
+      let val name = check_function ctxt arg
+      in ML_Syntax.atomic ("Scala.function_thread " ^ ML_Syntax.print_string name) end)));
 
 end;

--- a/src/Pure/System/scala.scala	Tue Sep 29 12:12:34 2020 +0200
+++ b/src/Pure/System/scala.scala	Tue Sep 29 13:19:34 2020 +0200
@@ -196,12 +196,18 @@
     private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized
     {
       msg.properties match {
-        case Markup.Invoke_Scala(name, id) =>
-          futures += (id ->
-            Future.fork {
-              val (tag, res) = Scala.function(name, msg.text)
-              result(id, tag, res)
-            })
+        case Markup.Invoke_Scala(name, id, thread) =>
+          def body
+          {
+            val (tag, res) = Scala.function(name, msg.text)
+            result(id, tag, res)
+          }
+          val future =
+            if (thread) {
+              Future.thread(name = Isabelle_Thread.make_name(base = "invoke_scala"))(body)
+            }
+            else Future.fork(body)
+          futures += (id -> future)
           true
         case _ => false
       }