# HG changeset patch
# User wenzelm
# Date 1638911503 -3600
# Node ID c49362e85f5a6fee647508a1c5ec9f5cab7bac95
# Parent  74a800810bde61a7ea9d7913da26d0cf50395ebd
proper ML types (amending 1aa92bc4d356);

diff -r 74a800810bde -r c49362e85f5a src/Doc/System/Scala.thy
--- a/src/Doc/System/Scala.thy	Tue Dec 07 22:04:46 2021 +0100
+++ b/src/Doc/System/Scala.thy	Tue Dec 07 22:11:43 2021 +0100
@@ -367,11 +367,12 @@
 
   \<^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. 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.
+  \<^ML_type>\<open>string list -> string list\<close> or \<^ML_type>\<open>string -> string\<close>,
+  depending on the definition in Isabelle/Scala. Evaluation 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. 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