discontinue old / inaccurate show_brackets (see also a4f09493d929 and ca9f5dbab880);

--- a/NEWS	Tue Jan 07 21:39:38 2025 +0100
+++ b/NEWS	Tue Jan 07 22:07:46 2025 +0100
@@ -82,6 +82,11 @@
 adapted accordingly, but it is often better to use "unbundle no
 foobar_syntax", as explained for HOL libraries below.
 
+* 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).
+
 * Command "unbundle b" and its variants like "context includes b" allow
 an optional name prefix with the reserved word "no": "unbundle no b"
 etc. This reverses both the order and polarity of bundled declarations
@@ -137,6 +142,7 @@
 'structure'). Rare INCOMPATIBILITY, e.g. in "subgoal_tac", "rule_tac".
 
 
+
 *** Isabelle/jEdit Prover IDE ***
 
 * Action isabelle.select_structure (with keyboard shortcut C+7) extends

--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Tue Jan 07 21:39:38 2025 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Tue Jan 07 22:07:46 2025 +0100
@@ -113,7 +113,6 @@
     @{attribute_def show_sorts} & : & \<open>attribute\<close> & default \<open>false\<close> \\
     @{attribute_def show_consts} & : & \<open>attribute\<close> & default \<open>false\<close> \\
     @{attribute_def show_abbrevs} & : & \<open>attribute\<close> & default \<open>true\<close> \\
-    @{attribute_def show_brackets} & : & \<open>attribute\<close> & default \<open>false\<close> \\
     @{attribute_def names_long} & : & \<open>attribute\<close> & default \<open>false\<close> \\
     @{attribute_def names_short} & : & \<open>attribute\<close> & default \<open>false\<close> \\
     @{attribute_def names_unique} & : & \<open>attribute\<close> & default \<open>true\<close> \\
@@ -158,13 +157,6 @@
 
   \<^descr> @{attribute show_abbrevs} controls folding of constant abbreviations.
 
-  \<^descr> @{attribute show_brackets} controls bracketing in pretty printed output.
-  If enabled, all sub-expressions of the pretty printing tree will be
-  parenthesized, even if this produces malformed term syntax! This crude way
-  of showing the internal structure of pretty printed entities may
-  occasionally help to diagnose problems with operator priorities, for
-  example.
-
   \<^descr> @{attribute names_long}, @{attribute names_short}, and @{attribute
   names_unique} control the way of printing fully qualified internal names in
   external form. See also \secref{sec:antiq} for the document antiquotation

--- a/src/Pure/Isar/attrib.ML	Tue Jan 07 21:39:38 2025 +0100
+++ b/src/Pure/Isar/attrib.ML	Tue Jan 07 22:07:46 2025 +0100
@@ -602,7 +602,6 @@
   register_config_bool Goal.quick_and_dirty #>
   register_config_bool Ast.trace #>
   register_config_bool Ast.stats #>
-  register_config_bool Printer.show_brackets #>
   register_config_bool Printer.show_sorts #>
   register_config_bool Printer.show_types #>
   register_config_bool Printer.show_markup #>

--- a/src/Pure/Syntax/printer.ML	Tue Jan 07 21:39:38 2025 +0100
+++ b/src/Pure/Syntax/printer.ML	Tue Jan 07 22:07:46 2025 +0100
@@ -7,7 +7,6 @@
 
 signature BASIC_PRINTER =
 sig
-  val show_brackets: bool Config.T
   val show_types: bool Config.T
   val show_sorts: bool Config.T
   val show_markup: bool Config.T
@@ -51,7 +50,6 @@
 
 (** options for printing **)
 
-val show_brackets = Config.declare_option_bool ("show_brackets", \<^here>);
 val show_types = Config.declare_option_bool ("show_types", \<^here>);
 val show_sorts = Config.declare_option_bool ("show_sorts", \<^here>);
 val show_markup_default = Unsynchronized.ref false;
@@ -236,8 +234,6 @@
 
 fun pretty {type_mode, curried} ctxt prtabs (ops: pretty_ops) =
   let
-    val show_brackets = Config.get ctxt show_brackets;
-
     val application =
       if type_mode then Syntax_Trans.tappl_ast_tr'
       else if curried then Syntax_Trans.applC_ast_tr'
@@ -297,9 +293,7 @@
 
     and parens p q a (symbs, args) constraint =
       let
-        val symbs' =
-          if p > q orelse (show_brackets andalso q <> 1000 andalso not (is_chain symbs))
-          then [Block (par_block, par_bg :: symbs @ [par_en])] else symbs;
+        val symbs' = if p > q then [Block (par_block, par_bg :: symbs @ [par_en])] else symbs;
         val output =
           (case constraint of
             SOME (Ast.Appl [Ast.Constant "_constrain", _, ty]) =>

--- a/src/Pure/Syntax/syntax_phases.ML	Tue Jan 07 21:39:38 2025 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue Jan 07 22:07:46 2025 +0100
@@ -432,8 +432,6 @@
           val errs = map snd (failed_results results');
           val checked = map snd (proper_results results');
           val checked_len = length checked;
-
-          val pretty_term = Syntax.pretty_term (Config.put Printer.show_brackets true ctxt);
         in
           if checked_len = 0 then
             report_result ctxt pos []
@@ -452,7 +450,7 @@
                 (("Ambiguous input\n" ^ string_of_int checked_len ^ " terms are type correct" ^
                   (if checked_len <= limit then ""
                    else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
-                  map (Pretty.string_of o Pretty.item o single o pretty_term)
+                  map (Pretty.string_of o Pretty.item o single o Syntax.pretty_term ctxt)
                     (take limit checked))))))]
         end handle ERROR msg => parse_failed ctxt pos msg kind)
   end;