# HG changeset patch # User wenzelm # Date 1601378374 -7200 # Node ID 319dd5c618a5f65747270f977341d521d3ece843 # Parent 850ba6d47300d3eaed858a081aa5086869f11590 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM; diff -r 850ba6d47300 -r 319dd5c618a5 NEWS --- 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 *** diff -r 850ba6d47300 -r 319dd5c618a5 etc/symbols --- 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 diff -r 850ba6d47300 -r 319dd5c618a5 src/Doc/System/Scala.thy --- 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"} & : & \ML_antiquotation\ \\ @{ML_antiquotation_def "scala"} & : & \ML_antiquotation\ \\ + @{ML_antiquotation_def "scala_thread"} & : & \ML_antiquotation\ \\ \end{matharray} \<^rail>\ - (@{ML_antiquotation scala_function} | @{ML_antiquotation scala}) - @{syntax embedded} + (@{ML_antiquotation scala_function} | + @{ML_antiquotation scala} | + @{ML_antiquotation scala_thread}) @{syntax embedded} \ \<^descr> \@{scala_function name}\ inlines the checked function name as ML string literal. - \<^descr> \@{scala name}\ invokes the checked function via the PIDE protocol. In - Isabelle/ML this appears as a function of type + \<^descr> \@{scala name}\ and \@{scala_thread name}\ invoke the checked function via + the PIDE protocol. In Isabelle/ML this appears as a function of type \<^ML_type>\string -> string\, which is subject to interrupts within the ML runtime environment as usual. A \<^scala>\null\ result in Scala raises an - exception \<^ML>\Scala.Null\ in ML. + exception \<^ML>\Scala.Null\ in ML. The execution of \@{scala}\ works via a + Scala future on a bounded thread farm, while \@{scala_thread}\ 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 diff -r 850ba6d47300 -r 319dd5c618a5 src/Pure/PIDE/markup.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"); diff -r 850ba6d47300 -r 319dd5c618a5 src/Pure/PIDE/markup.scala --- 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 } } diff -r 850ba6d47300 -r 319dd5c618a5 src/Pure/System/scala.ML --- 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>\scala\ (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>\scala_thread\ + (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; diff -r 850ba6d47300 -r 319dd5c618a5 src/Pure/System/scala.scala --- 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 }