# HG changeset patch
# User wenzelm
# Date 1590588565 -7200
# Node ID 0dc67ae4a4c7c7bb5c50f996d68a4c40a9df2157
# Parent  64c9628b39fc8f041902b9252353d3c74fcf6427
more NEWS;

diff -r 64c9628b39fc -r 0dc67ae4a4c7 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