# HG changeset patch
# User wenzelm
# Date 1615635384 -3600
# Node ID 22f3f2117ed7f613aa33a6ddea5c20dcdd56756e
# Parent  7d7d959547a16f8fe3a9a73995388c490f0297da
clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;

diff -r 7d7d959547a1 -r 22f3f2117ed7 src/Doc/System/Scala.thy
--- a/src/Doc/System/Scala.thy	Fri Mar 12 23:30:35 2021 +0100
+++ b/src/Doc/System/Scala.thy	Sat Mar 13 12:36:24 2021 +0100
@@ -210,13 +210,11 @@
   \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} |
-     @{ML_antiquotation scala_thread}) @{syntax embedded}
+     @{ML_antiquotation scala}) @{syntax embedded}
   \<close>
 
   \<^descr> \<open>@{scala_function name}\<close> inlines the checked function name as ML string
diff -r 7d7d959547a1 -r 22f3f2117ed7 src/HOL/Tools/ATP/system_on_tptp.ML
--- a/src/HOL/Tools/ATP/system_on_tptp.ML	Fri Mar 12 23:30:35 2021 +0100
+++ b/src/HOL/Tools/ATP/system_on_tptp.ML	Sat Mar 13 12:36:24 2021 +0100
@@ -15,6 +15,6 @@
 
 fun get_url () = Options.default_string \<^system_option>\<open>SystemOnTPTP\<close>
 
-fun list_systems () = get_url () |> \<^scala_thread>\<open>SystemOnTPTP.list_systems\<close> |> split_lines
+fun list_systems () = get_url () |> \<^scala>\<open>SystemOnTPTP.list_systems\<close> |> split_lines
 
 end
diff -r 7d7d959547a1 -r 22f3f2117ed7 src/HOL/Tools/ATP/system_on_tptp.scala
--- a/src/HOL/Tools/ATP/system_on_tptp.scala	Fri Mar 12 23:30:35 2021 +0100
+++ b/src/HOL/Tools/ATP/system_on_tptp.scala	Sat Mar 13 12:36:24 2021 +0100
@@ -29,7 +29,7 @@
     proper_lines(result.text)
   }
 
-  object List_Systems extends Scala.Fun("SystemOnTPTP.list_systems")
+  object List_Systems extends Scala.Fun("SystemOnTPTP.list_systems", thread = true)
   {
     val here = Scala_Project.here
     def apply(url: String): String = cat_lines(list_systems(Url(url)))
diff -r 7d7d959547a1 -r 22f3f2117ed7 src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Fri Mar 12 23:30:35 2021 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Sat Mar 13 12:36:24 2021 +0100
@@ -1035,7 +1035,7 @@
             (timeout, (solve_all, (max_solutions, (max_threads, kki))))
             |> let open XML.Encode in pair int (pair bool (pair int (pair int string))) end
             |> YXML.string_of_body
-            |> \<^scala_thread>\<open>kodkod\<close>
+            |> \<^scala>\<open>kodkod\<close>
             |> YXML.parse_body
             |> let open XML.Decode in triple int string string end
 
diff -r 7d7d959547a1 -r 22f3f2117ed7 src/HOL/Tools/Nitpick/kodkod.scala
--- a/src/HOL/Tools/Nitpick/kodkod.scala	Fri Mar 12 23:30:35 2021 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.scala	Sat Mar 13 12:36:24 2021 +0100
@@ -154,7 +154,7 @@
 
   /** scala function **/
 
-  object Fun extends Scala.Fun("kodkod")
+  object Fun extends Scala.Fun("kodkod", thread = true)
   {
     val here = Scala_Project.here
     def apply(args: String): String =
diff -r 7d7d959547a1 -r 22f3f2117ed7 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Fri Mar 12 23:30:35 2021 +0100
+++ b/src/Pure/PIDE/markup.ML	Sat Mar 13 12:36:24 2021 +0100
@@ -215,7 +215,7 @@
   val commands_accepted: Properties.T
   val assign_update: Properties.T
   val removed_versions: Properties.T
-  val invoke_scala: string -> string -> bool -> Properties.T
+  val invoke_scala: string -> string -> Properties.T
   val cancel_scala: string -> Properties.T
   val task_statistics: Properties.entry
   val command_timing: Properties.entry
@@ -683,8 +683,7 @@
 val assign_update = [(functionN, "assign_update")];
 val removed_versions = [(functionN, "removed_versions")];
 
-fun invoke_scala name id thread =
-  [(functionN, "invoke_scala"), (nameN, name), (idN, id), ("thread", Value.print_bool thread)];
+fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
 
 fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
 
diff -r 7d7d959547a1 -r 22f3f2117ed7 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Fri Mar 12 23:30:35 2021 +0100
+++ b/src/Pure/PIDE/markup.scala	Sat Mar 13 12:36:24 2021 +0100
@@ -636,10 +636,9 @@
 
   object Invoke_Scala extends Function("invoke_scala")
   {
-    def unapply(props: Properties.T): Option[(String, String, Boolean)] =
+    def unapply(props: Properties.T): Option[(String, String)] =
       props match {
-        case List(PROPERTY, (NAME, name), (ID, id), ("thread", Value.Boolean(thread))) =>
-          Some((name, id, thread))
+        case List(PROPERTY, (NAME, name), (ID, id)) => Some((name, id))
         case _ => None
       }
   }
diff -r 7d7d959547a1 -r 22f3f2117ed7 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Fri Mar 12 23:30:35 2021 +0100
+++ b/src/Pure/PIDE/resources.ML	Sat Mar 13 12:36:24 2021 +0100
@@ -200,11 +200,7 @@
   ML_Antiquotation.value_embedded \<^binding>\<open>scala\<close>
     (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) =>
       let val name = check_scala_function ctxt arg
-      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_scala_function ctxt arg
-      in ML_Syntax.atomic ("Scala.function_thread " ^ ML_Syntax.print_string name) end)));
+      in ML_Syntax.atomic ("Scala.function " ^ ML_Syntax.print_string name) end)));
 
 
 (* manage source files *)
diff -r 7d7d959547a1 -r 22f3f2117ed7 src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Fri Mar 12 23:30:35 2021 +0100
+++ b/src/Pure/System/bash.scala	Sat Mar 13 12:36:24 2021 +0100
@@ -206,7 +206,7 @@
 
   /* Scala function */
 
-  object Process extends Scala.Fun("bash_process")
+  object Process extends Scala.Fun("bash_process", thread = true)
   {
     val here = Scala_Project.here
     def apply(script: String): String =
diff -r 7d7d959547a1 -r 22f3f2117ed7 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Fri Mar 12 23:30:35 2021 +0100
+++ b/src/Pure/System/isabelle_system.ML	Sat Mar 13 12:36:24 2021 +0100
@@ -28,7 +28,7 @@
 (* bash *)
 
 fun bash_process script =
-  Scala.function_thread "bash_process"
+  Scala.function "bash_process"
     ("export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP") ^ "\n" ^ script)
   |> split_strings0
   |> (fn [] => raise Exn.Interrupt
@@ -112,6 +112,6 @@
 (* download file *)
 
 fun download url file =
-  ignore (Scala.function_thread "download" (cat_strings0 [url, absolute_path file]));
+  ignore (Scala.function "download" (cat_strings0 [url, absolute_path file]));
 
 end;
diff -r 7d7d959547a1 -r 22f3f2117ed7 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Fri Mar 12 23:30:35 2021 +0100
+++ b/src/Pure/System/isabelle_system.scala	Sat Mar 13 12:36:24 2021 +0100
@@ -557,7 +557,7 @@
     Bytes.write(file, content.bytes)
   }
 
-  object Download extends Scala.Fun("download")
+  object Download extends Scala.Fun("download", thread = true)
   {
     val here = Scala_Project.here
     def apply(arg: String): String =
diff -r 7d7d959547a1 -r 22f3f2117ed7 src/Pure/System/scala.ML
--- a/src/Pure/System/scala.ML	Fri Mar 12 23:30:35 2021 +0100
+++ b/src/Pure/System/scala.ML	Sat Mar 13 12:36:24 2021 +0100
@@ -8,7 +8,6 @@
 sig
   exception Null
   val function: string -> string -> string
-  val function_thread: string -> string -> string
 end;
 
 structure Scala: SCALA =
@@ -37,13 +36,15 @@
           | _ => raise Fail ("Bad tag: " ^ tag));
       in Synchronized.change results (Symtab.map_entry id (K result)) end);
 
-fun gen_function thread name arg =
+in
+
+fun function 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 thread) [XML.Text arg]);
+        Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg]);
       fun cancel () =
        (Synchronized.change results (Symtab.delete_safe id);
         Output.protocol_message (Markup.cancel_scala id) []);
@@ -60,11 +61,6 @@
         handle exn => (if Exn.is_interrupt exn then cancel () else (); Exn.reraise exn)
     end) ();
 
-in
-
-val function = gen_function false;
-val function_thread = gen_function true;
-
 end;
 
 end;
diff -r 7d7d959547a1 -r 22f3f2117ed7 src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Fri Mar 12 23:30:35 2021 +0100
+++ b/src/Pure/System/scala.scala	Sat Mar 13 12:36:24 2021 +0100
@@ -17,7 +17,8 @@
 {
   /** registered functions **/
 
-  abstract class Fun(val name: String) extends Function[String, String]
+  abstract class Fun(val name: String, val thread: Boolean = false)
+    extends Function[String, String]
   {
     override def toString: String = name
     def position: Properties.T = here.position
@@ -155,7 +156,13 @@
     val NULL, OK, ERROR, FAIL, INTERRUPT = Value
   }
 
-  def function(name: String, arg: String): (Tag.Value, String) =
+  def function_thread(name: String): Boolean =
+    functions.find(fun => fun.name == name) match {
+      case Some(fun) => fun.thread
+      case None => false
+    }
+
+  def function_body(name: String, arg: String): (Tag.Value, String) =
     functions.find(fun => fun.name == name) match {
       case Some(fun) =>
         Exn.capture { fun(arg) } match {
@@ -202,14 +209,14 @@
     private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized
     {
       msg.properties match {
-        case Markup.Invoke_Scala(name, id, thread) =>
+        case Markup.Invoke_Scala(name, id) =>
           def body: Unit =
           {
-            val (tag, res) = Scala.function(name, msg.text)
+            val (tag, res) = Scala.function_body(name, msg.text)
             result(id, tag, res)
           }
           val future =
-            if (thread) {
+            if (Scala.function_thread(name)) {
               Future.thread(name = Isabelle_Thread.make_name(base = "invoke_scala"))(body)
             }
             else Future.fork(body)