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 \Defining functions in Isabelle/Scala\ text \ - A Scala functions of type \<^scala_type>\String => String\ may be wrapped as - \<^scala_type>\isabelle.Scala.Fun\ and collected via an instance of the - class \<^scala_type>\isabelle.Scala.Functions\. A system component can then - register that class via \<^verbatim>\services\ in \<^path>\etc/build.props\ - (\secref{sec:scala-build}). An example is the predefined collection of - \<^scala_type>\isabelle.Scala.Functions\ in \<^file>\$ISABELLE_HOME/etc/build.props\. + The service class \<^scala_type>\isabelle.Scala.Functions\ collects Scala + functions of type \<^scala_type>\isabelle.Scala.Fun\: by registering + instances via \<^verbatim>\services\ in \<^path>\etc/build.props\ + (\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>\isabelle.Scala.Functions\ in + \<^file>\$ISABELLE_HOME/etc/build.props\. The overall list of registered functions + is accessible in Isabelle/Scala as \<^scala_object>\isabelle.Scala.functions\. + + The general class \<^scala_type>\isabelle.Scala.Fun\ expects a multi-argument + / multi-result function + \<^scala_type>\List[isabelle.Bytes] => List[isabelle.Bytes]\; more common are + instances of \<^scala_type>\isabelle.Scala.Fun_Strings\ for type + \<^scala_type>\List[String] => List[String]\, or + \<^scala_type>\isabelle.Scala.Fun_String\ for type + \<^scala_type>\String => String\. \