[isabelle-dev] NEWS: Type constraints for constants (inner syntax printing)

[Makarius]

On 17/10/2024 11:12, Norbert Schirmer wrote:
> I guess you wanted to mention this News entry:
> 
> * Inner syntax printing now supports type constraints for constants:
> this is guarded by the configuration options "show_consts_markup"
> (default true) and "show_markup" (default true for PIDE interaction).
> Ast translation rules (command 'translations') and mixfix notation work
> with or without such extra constraints, but ML translation functions
> (command 'print_ast_translation') need may need to be changed slightly.
> Rare INCOMPATIBILITY. The Prover IDE displays type constraints for
> constants as for variables, e.g. via C-mouse hovering.

You are right. Here is an updated version:

* Inner syntax printing now supports type constraints for constants,
optionally with mixfix syntax (infix, binder etc.). This is guarded by
the configuration options "show_consts_markup" (default true) and
"show_markup" (default true for PIDE interaction). The Prover IDE
displays type constraints as usual via C-mouse hovering. Ast translation
rules (command 'translations') already work with extra type constraints,
but the result omits the type of a matched constant. ML translation
functions (command 'print_ast_translation') based on Ast.unfold_ast etc.
work in the same manner, but more complex translations may require
manual changes: rare INCOMPATIBILITY.

See Isabelle/0e27325da568.


After so many renovations of the inner-syntax engine, old problems get 
actually solved, although it has required some decades.

Now the situation is again asymmetric, because mixfix consts don't get type 
constraints on input.


	Makarius