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

[Makarius]

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

Further side-remarks:

   * "output" means that I have reworked to Pretty-printing engine quite a 
bit, to be more robust and scalable for tons of markup (lets say many MB up to 
few GB).

   * "input" means that I have applied approx. 60 small changes to 
src/Pure/Syntax/parser.ML in order to have markup treated properly within the 
regular Earley algorithm. I have discovered and removed various oddities in 
the implementation, but did not understand all of its secrets. As usual, the 
empiric test material was AFP (including performance).


The markup for input was specifically requested by people from Linz, as a 
prerequisite to make an "accessible" Prover IDE eventually. It means that 
users without eyesight can explore types/terms/props by a tactile interface. 
(A few years ago VSCode had made quite some noise about "accessibility", but 
that has degraded a lot recently, so it is not an immediate answer to the 
problem.)


	Makarius