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

[Makarius]

On 10/10/2024 14:25, Makarius wrote:
> 
> * 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.

Some more remarks on this. Markup for pretty-blocks (or quasi blocks via 
"open_block") replaces the old TODO-item of "markup of sub-expressions of 
types/terms/blocks". The latter turned out as too complex to be ever 
implemented, especially due to very ambitious syntax translations that have 
emerged over the decades in applications.

Doing it on the surface of the inner-syntax instead, merely required some 
"minor" cleanup and manual annotations of free-form mixfix syntax (not infix 
nor binder). I have mostly done it for the main Isabelle library theories 
already: HOL, HOL-Library, HOL-Algebra, HOL-Number_Theory, HOL-Analysis etc. 
More isolated applications are missing, as well as most of AFP.

Some important inner-syntax idioms --- e.g. monad syntax and Hoare-logic 
syntax --- still require further refinement. Ultimately, there should be just 
one well-understood and uniform approach to it, not 3 different approaches to 
7 different versions monads or Hoare logic.


	Makarius