
diff -r bdaf29253394 -r 74a800810bde src/Doc/System/Scala.thy
--- a/src/Doc/System/Scala.thy	Tue Dec 07 19:32:43 2021 +0100
+++ b/src/Doc/System/Scala.thy	Tue Dec 07 22:04:46 2021 +0100
@@ -321,15 +321,25 @@
 subsection \<open>Defining functions in Isabelle/Scala\<close>
 
 text \<open>
-  A Scala functions of type \<^scala_type>\<open>String => String\<close> may be wrapped as
-  \<^scala_type>\<open>isabelle.Scala.Fun\<close> and collected via an instance of the
-  class \<^scala_type>\<open>isabelle.Scala.Functions\<close>. A system component can then
-  register that class via \<^verbatim>\<open>services\<close> in \<^path>\<open>etc/build.props\<close>
-  (\secref{sec:scala-build}). An example is the predefined collection of
-  \<^scala_type>\<open>isabelle.Scala.Functions\<close> in \<^file>\<open>$ISABELLE_HOME/etc/build.props\<close>.
+  The service class \<^scala_type>\<open>isabelle.Scala.Functions\<close> collects Scala
+  functions of type \<^scala_type>\<open>isabelle.Scala.Fun\<close>: by registering
+  instances via \<^verbatim>\<open>services\<close> in \<^path>\<open>etc/build.props\<close>
+  (\secref{sec:scala-build}), it is becomes possible to invoke Isabelle/Scala
+  from Isabelle/ML (see below).
 
-  The overall list of registered functions is accessible in Isabelle/Scala as
+  An example is the predefined collection of
+  \<^scala_type>\<open>isabelle.Scala.Functions\<close> in
+  \<^file>\<open>$ISABELLE_HOME/etc/build.props\<close>. The overall list of registered functions
+  is accessible in Isabelle/Scala as
   \<^scala_object>\<open>isabelle.Scala.functions\<close>.
+
+  The general class \<^scala_type>\<open>isabelle.Scala.Fun\<close> expects a multi-argument
+  / multi-result function
+  \<^scala_type>\<open>List[isabelle.Bytes] => List[isabelle.Bytes]\<close>; more common are
+  instances of \<^scala_type>\<open>isabelle.Scala.Fun_Strings\<close> for type
+  \<^scala_type>\<open>List[String] => List[String]\<close>, or
+  \<^scala_type>\<open>isabelle.Scala.Fun_String\<close> for type
+  \<^scala_type>\<open>String => String\<close>.
 \<close>
 
 




