more NEWS;
authorwenzelm
Wed, 27 May 2020 16:09:25 +0200
changeset 72135 0dc67ae4a4c7
parent 72134 64c9628b39fc
child 72136 cdcf2fcf3f54
more NEWS;
NEWS
--- 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