[isabelle-dev] Remaining uses of show_brackets

[Makarius]

On 11/10/2024 10:45, Peter Lammich wrote:
>>
>> 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

So now is a good oppurtinity to try the new markup scheme of 
Isabelle/87f173836d56.

It can save a lot of time, because things don't have to be printed to see the 
term structure.


	Makarius