[isabelle-dev] NEWS: Dependencies and markup for inner syntax translations

[Makarius]

** General **

* 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.

This refers to Isabelle/bcecb69f72fa and AFP/c69af9cd3390.

I have already adapted the majority of existing translations, but this 
excludes very ambitious ones with pages of translation rules or ML translation 
functions. It does require some understanding of what is intended! 
Occasionally it also requires minor changes of syntax, e.g. see 
Isabelle/66a8113ac23e for enumeration syntax of set, list, tuples.

Hopefully the topic can now be closed, and I won't have to improve scalability 
of pretty printing further (beyond Isabelle/bcecb69f72fa): Having more markup 
means that message / XML trees become larger, and applications that explore 
the border of the inhabitable area of Isabelle might fall over.


	Makarius