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