[isabelle-dev] NEWS: Inner-syntax markup and declaration bundles

[Makarius]

*** General ***

* Command "unbundle b" and its variants like "context includes b" allow
an optional name prefix with the reserved word "no": "unbundle no b"
etc. This inverts the polarity of bundled declarations like 'notation'
vs. 'no_notation', and thus avoids redundant bundle definitions like
"foobar_syntax" vs. "no_foobar_syntax", because "no foobar_syntax" may
be used instead. Consequently, the syntax for multiple bundle names has
been changed slightly, demanding an explicit 'and' keyword. Minor
INCOMPATIBILITY.

* Command "open_bundle b" is like "bundle b" followed by "unbundle b",
so its declarations are applied immediately, but also named for later
re-use: "unbundle no b" etc.

* Blocks for pretty-printing (of types, terms, props etc.) now support
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). Occasional
INCOMPATIBILITY for 'no_syntax' or 'no_notation' declarations in user
applications: the mixfix template needs to be adapted accordingly, but
it is often better to use "unbundle no foobar_syntax", as explained for
HOL libraries below.

* Inner syntax translations now support formal dependencies via commands
'syntax_types' or 'syntax_consts'. This is essentially an abstract
specification of the effect of 'translations' (or translation functions
in ML). Most Isabelle theories have been adapted accordingly, such that
hyperlinks work properly e.g. for "['a, 'b] ⇒ 'c" or "⟦A; B⟧ ⟹ C" in
Pure, and "∀x∈A. B x" or "∃x∈A. B x" in HOL.


*** HOL ***

* Various declaration bundles support adhoc modification of notation,
notably like this:

   unbundle no list_syntax
   unbundle no list_enumeration_syntax
   unbundle no list_comprehension_syntax
   unbundle no relcomp_syntax
   unbundle no converse_syntax
   unbundle no rtrancl_syntax
   unbundle no trancl_syntax
   unbundle no reflcl_syntax
   unbundle no abs_syntax
   unbundle no floor_ceiling_syntax
   unbundle no uminus_syntax
   unbundle no funcset_syntax

This is more robust than individual 'no_syntax' / 'no_notation'
commands, which need to copy mixfix declarations from elsewhere and thus
break after changes in the library.

* Theory "HOL-Library.Datatype_Records" provides bundle
"datatype_record_syntax" to exchange its alternative notation versus
regular "record_syntax". This also allows to swap record syntax later
on, notably like this:

   unbundle no datatype_record_syntax


This refers to Isabelle/87f173836d56 and AFP/68a8276e79a0.


	Makarius