Remaining uses of show_brackets

[Makarius]

On 10/10/2024 20:16, Makarius wrote:
> So if there are no further uses of it, I will remove it shortly before the 
> Isabelle2025 release process starts (Jan-2025).

I have now removed it shortly after RC0: 
https://isabelle-dev.sketis.net/rISABELLEfac2045e61d5

The corresponding NEWS entry reads:

"""
* The option "show_brackets" has been discontinued: its inaccurate
placement of extra parentheses has been superseded by markup of mixfix
blocks (which allows to explore subterm structure in the Prover IDE via
C-mouse hovering).
"""


It turned out that its only remaining use within the Isabelle sources was the 
printing of multiple ambiguously parsed terms, see this change from 1994: 
https://isabelle-dev.sketis.net/rISABELLEca9f5dbab880

All this should now work better with the new mixfix block markup. In output, 
the Prover IDE shows it by default, when moving the mouse over it.


(If other remaining uses of show_brackets show up, we still have time until 
RC1/RC2/RC3 to sort it out.)


	Makarius