# HG changeset patch
# User wenzelm
# Date 1639304322 -3600
# Node ID cdd2284c8047054ff24e54bfa66631204d96363d
# Parent  70be57333ea1b0e1866be2e944f2e0f70c437ae4# Parent  0dd4dbe7bed387ab84124eac5ad991486698062c
merged, resolving conflict in src/Doc/Implementation/Logic.thy;

diff -r 0dd4dbe7bed3 -r cdd2284c8047 .hgtags
--- a/.hgtags	Sat Dec 11 11:17:36 2021 +0100
+++ b/.hgtags	Sun Dec 12 11:18:42 2021 +0100
@@ -44,3 +44,4 @@
 2b212c8138a57096487461fa353386f753ff7a11 Isabelle2021-1-RC3
 2336356d4180b948eb9070f3f9f8986cda7e8f76 Isabelle2021-1-RC4
 8baf2e8b16e2218edaeb6dee402b21f97a49a505 Isabelle2021-1-RC5
+c2a2be496f35aa1a6072393aebfdb1b85c9f2e9e Isabelle2021-1
diff -r 0dd4dbe7bed3 -r cdd2284c8047 ANNOUNCE
--- a/ANNOUNCE	Sat Dec 11 11:17:36 2021 +0100
+++ b/ANNOUNCE	Sun Dec 12 11:18:42 2021 +0100
@@ -38,8 +38,9 @@
 
 * System: improved document preparation using Isabelle/Scala.
 
-* System: update to current OpenJDK 17 (LTS) and Poly/ML 5.9 (with preliminary
-support for arm64).
+* System: update to current Java 17 LTS.
+
+* System: update to Poly/ML 5.9 with improved support for ARM64 on Linux.
 
 
 You may get Isabelle2021-1 from the following mirror sites:
diff -r 0dd4dbe7bed3 -r cdd2284c8047 src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Sat Dec 11 11:17:36 2021 +0100
+++ b/src/Doc/Implementation/Logic.thy	Sun Dec 12 11:18:42 2021 +0100
@@ -492,7 +492,7 @@
       @{syntax name} (@{syntax embedded_ml}*) (@{syntax for_args})?
     ;
     @{syntax_def term_const_fn}:
-      @{ syntax term_const} @'=>' @{syntax embedded_ml}
+      @{syntax term_const} @'=>' @{syntax embedded_ml}
     ;
     @{syntax_def for_args}: @'for' (@{syntax embedded_ml}+)
   \<close>
diff -r 0dd4dbe7bed3 -r cdd2284c8047 src/Doc/System/Scala.thy
--- a/src/Doc/System/Scala.thy	Sat Dec 11 11:17:36 2021 +0100
+++ b/src/Doc/System/Scala.thy	Sun Dec 12 11:18:42 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>
 
 
@@ -357,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