Stream: Mirror: Isabelle Development Mailing List

Topic: Remaining uses of show_brackets

Email Gateway (Jan 07 2025 at 22:18):

From: Makarius <makarius@sketis.net>
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

Last updated: Feb 01 2025 at 20:19 UTC