--- a/NEWS Wed May 27 16:05:17 2020 +0200
+++ b/NEWS Wed May 27 16:09:25 2020 +0200
@@ -9,8 +9,11 @@
*** Document preparation ***
-* Antiquotation @{bash_function NAME} prints the given GNU bash function
-verbatim --- checked against the Isabelle settings environment.
+* Antiquotation @{bash_function} refers to GNU bash functions that are
+checked within the Isabelle settings environment.
+
+* Antiquotations @{scala}, @{scala_object}, @{scala_type},
+@{scala_method} refer to checked Isabelle/Scala entities.
*** Pure ***
@@ -38,6 +41,13 @@
* Added the "at most 1" quantifier, Uniq, as in HOL.
+*** ML ***
+
+* Antiquotations @{scala_function NAME} and @{scala NAME} refer to
+registered Isabelle/Scala functions (of type String => String):
+invocation works via the PIDE protocol.
+
+
*** System ***
* The command-line tool "isabelle console" now supports interrupts