[isabelle-dev] Remaining uses of show_brackets

[Makarius]

Are there any remaining uses of show_brackets?


Here is historical proof for this feature from many decades ago:

changeset:   504:a4f09493d929
user:        nipkow
date:        Tue Aug 02 09:07:10 1994 +0200
files:       src/Pure/Syntax/printer.ML
description:
added flag show_brackets for printinmg fully bracketed terms.

changeset:   508:d8b6999ca364
user:        lcp
date:        Thu Aug 04 11:51:30 1994 +0200
files:       doc-src/Ref/introduction.tex
description:
addition of show_brackets

The documentation in d8b6999ca364 says: "show_brackets makes Isabelle show 
full bracketing.  This reveals the grouping of infix operators."

We have that already via PIDE markup for pretty-blocks, see also 
Isabelle/87f173836d56 --- and it works more accurately, too.


So if there are no further uses of it, I will remove it shortly before the 
Isabelle2025 release process starts (Jan-2025).


	Makarius