# HG changeset patch
# User wenzelm
# Date 1728511189 -7200
# Node ID 20ca8aa4b7ca365fb924ac5f5f5cf33ab6ec99ac
# Parent  6ad2c917dd2e7ea6751b69ac9be6f2a5c8d07c63
more NEWS;

diff -r 6ad2c917dd2e -r 20ca8aa4b7ca NEWS
--- a/NEWS	Wed Oct 09 23:38:29 2024 +0200
+++ b/NEWS	Wed Oct 09 23:59:49 2024 +0200
@@ -23,9 +23,17 @@
 re-use: "unbundle no b" etc.
 
 * Blocks for pretty-printing (of types, terms, props etc.) now support
-the option "open_block". Thus the block has no impact on formatting, but
-it may carry markup information, which is relevant both for input and
-output of inner syntax.
+properties "open_block" (bool) and "notation" (string as cartouche).
+When "open_block" is enabled, the block has no impact on formatting, but
+it may carry markup information via "notation". The latter uses formal
+kinds (e.g. "mixfix", "infix", "binder") together with informal words to
+describe the notation. This markup affects both input and output of
+inner syntax --- it can be explored via mouse hovering in the Prover IDE
+as usual (or programmatically by Isabelle/Scala tools). Markup for
+"infix" and "binder" declarations are automatic, but general mixfix
+forms require manual annotations in the theory library. Plenty of
+existing examples may be found in the Isabelle sources by searching for
+"notation=" (without quotes and no extra space).
 
 * Inner syntax translations now support formal dependencies via commands
 'syntax_types' or 'syntax_consts'. This is essentially an abstract