# 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}+) \ 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 \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\. \ @@ -357,11 +367,12 @@ \<^descr> \@{scala name}\ and \@{scala_thread name}\ invoke the checked function via the PIDE protocol. In Isabelle/ML this appears as a function of type - \<^ML_type>\string -> string\, which is subject to interrupts within the ML - runtime environment as usual. A \<^scala>\null\ result in Scala raises an - exception \<^ML>\Scala.Null\ in ML. The execution of \@{scala}\ works via a - Scala future on a bounded thread farm, while \@{scala_thread}\ always forks - a separate Java thread. + \<^ML_type>\string list -> string list\ or \<^ML_type>\string -> string\, + depending on the definition in Isabelle/Scala. Evaluation is subject to + interrupts within the ML runtime environment as usual. A \<^scala>\null\ + result in Scala raises an exception \<^ML>\Scala.Null\ in ML. The execution + of \@{scala}\ works via a Scala future on a bounded thread farm, while + \@{scala_thread}\ 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