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

[Lawrence Paulson]

Many thanks for this. A recurring problem I see is people using precedences incorrectly, resulting in highly ambiguous grammars. One sees formulas with dozens of parse trees. This might be another task for the linter, if it can be done.

Larry

> On 29 Aug 2024, at 21:47, Makarius <makarius at sketis.net> wrote:
>
> ** 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev