[isabelle-dev] Remaining uses of show_brackets

[Makarius]

On 11/10/2024 13:41, Lawrence Paulson wrote:
> I tried it on a set comprehension and got
> 
> 	notation: mixfix "set comprehension”
> 
> This is pretty useful, because in the past there was no way to examine non-trivial syntax constructions, which in some cases were a complete mystery.
> 
> If it's not too difficult, could it be possible to jump to the original definition?

That is also possible: I've actually had that before setting out for all this 
"notation=..." markup. It is merely a matter of adding 'syntax_consts' 
declarations, like I've always done for "notation=binder" to imitate regular 
'binder' declarations. You can see that e.g. in prop "∀x∈A. P x"

A minor disadvantage: the present PIDE rendering sometimes hides markup that 
is stacked up too ambitiously, and there is no whitespace between tokens to 
hover over it.

So I will keep this on the TODO list to think about further ...


	Makarius