[isabelle-dev] Remaining uses of show_brackets

[Lawrence Paulson]

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?

Larry

> On 11 Oct 2024, at 09:13, Makarius <makarius at sketis.net> wrote:
> 
> Can you try if the new mixfix markup works sufficiently well to replace this idea? The new scheme works for parsed input source and pretty-printed output. You just C-hover over the text, and get feedback about its inner-syntax structure.