[isabelle-dev] Remaining uses of show_brackets

[Peter Lammich]

On 11/10/2024 10:13, Makarius wrote:
> >> 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?

If I'm unsure about operator precedence, I usually go the other way 
round: I manually add some parentheses, and see how/if the 
pretty-printed term changes

--

   Peter



>
> 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
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev