--- 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