[isabelle-dev] Remaining uses of show_brackets

[Makarius]

 >> On 10 Oct 2024, at 19:51, Makarius <makarius at sketis.net> wrote:
 >>
 >> I don't understand what you mean by "legible". How is the following 
example legible?
 >>
 >> declare [[show_brackets]]
 >> lemma ‹∀x y. P x y ⟶ Q y x›
 >>
 >> goal (1 subgoal):
 >> 1. (∀(x y). ((P x y) ⟶ (Q y x)))

On 10/10/2024 22:48, Lawrence Paulson wrote:
> Oh, that one. I quite forgot it was there. But it’s occasionally useful when you aren’t sure about operator precedences. Is it hard to support?

It is a totally adhoc feature from 30 years ago, and incorrect in certain 
situations.

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.

People might call that a "parse tree", but it is better than a raw parse tree 
(which contains a lot of irrelevant information).


	Makarius