# HG changeset patch # User wenzelm # Date 1736284066 -3600 # Node ID fac2045e61d576f2dce41716c9dbdf9b7d626e5a # Parent 4b739ed65946b80f811bb163e4b5366c3b0e3605 discontinue old / inaccurate show_brackets (see also a4f09493d929 and ca9f5dbab880); diff -r 4b739ed65946 -r fac2045e61d5 NEWS --- 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 diff -r 4b739ed65946 -r fac2045e61d5 src/Doc/Isar_Ref/Inner_Syntax.thy --- 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} & : & \attribute\ & default \false\ \\ @{attribute_def show_consts} & : & \attribute\ & default \false\ \\ @{attribute_def show_abbrevs} & : & \attribute\ & default \true\ \\ - @{attribute_def show_brackets} & : & \attribute\ & default \false\ \\ @{attribute_def names_long} & : & \attribute\ & default \false\ \\ @{attribute_def names_short} & : & \attribute\ & default \false\ \\ @{attribute_def names_unique} & : & \attribute\ & default \true\ \\ @@ -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 diff -r 4b739ed65946 -r fac2045e61d5 src/Pure/Isar/attrib.ML --- 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 #> diff -r 4b739ed65946 -r fac2045e61d5 src/Pure/Syntax/printer.ML --- 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]) => diff -r 4b739ed65946 -r fac2045e61d5 src/Pure/Syntax/syntax_phases.ML --- 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;