# HG changeset patch # User wenzelm # Date 1291305172 -3600 # Node ID ca132ef449440ab0a97a2613065315b9a173cfcf # Parent 7695e4de4d8658cc45b46a0b6bf5106e1d2f5e81 configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning; diff -r 7695e4de4d86 -r ca132ef44944 NEWS --- a/NEWS Thu Dec 02 16:04:22 2010 +0100 +++ b/NEWS Thu Dec 02 16:52:52 2010 +0100 @@ -34,8 +34,8 @@ * Various options that affect pretty printing etc. are now properly handled within the context via configuration options, instead of -unsynchronized references. There are both ML Config.T entities and -Isar declaration attributes to access these. +unsynchronized references or print modes. There are both ML Config.T +entities and Isar declaration attributes to access these. ML (Config.T) Isar (attribute) @@ -45,6 +45,7 @@ show_types show_types show_question_marks show_question_marks show_consts show_consts + show_abbrevs show_abbrevs Syntax.ambiguity_level syntax_ambiguity_level @@ -59,6 +60,8 @@ Note that corresponding "..._default" references in ML may be only changed globally at the ROOT session setup, but *not* within a theory. +The option "show_abbrevs" supersedes the former print mode +"no_abbrevs" with inverted meaning. * More systematic naming of some configuration options. INCOMPATIBILTY. diff -r 7695e4de4d86 -r ca132ef44944 doc-src/IsarRef/Thy/Document_Preparation.thy --- a/doc-src/IsarRef/Thy/Document_Preparation.thy Thu Dec 02 16:04:22 2010 +0100 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Thu Dec 02 16:52:52 2010 +0100 @@ -339,6 +339,9 @@ \item @{antiquotation_option_def show_structs}~@{text "= bool"} controls printing of implicit structures. + \item @{antiquotation_option_def show_abbrevs}~@{text "= bool"} + controls folding of abbreviations. + \item @{antiquotation_option_def long_names}~@{text "= bool"} forces names of types and constants etc.\ to be printed in their fully qualified internal form. diff -r 7695e4de4d86 -r ca132ef44944 doc-src/IsarRef/Thy/Inner_Syntax.thy --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Dec 02 16:04:22 2010 +0100 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Dec 02 16:52:52 2010 +0100 @@ -99,6 +99,7 @@ @{index_ML show_types: "bool Config.T"} & default @{ML false} \\ @{index_ML show_sorts: "bool Config.T"} & default @{ML false} \\ @{index_ML show_consts: "bool Config.T"} & default @{ML false} \\ + @{index_ML show_abbrevs: "bool Config.T"} & default @{ML true} \\ @{index_ML long_names: "bool Unsynchronized.ref"} & default @{ML false} \\ @{index_ML short_names: "bool Unsynchronized.ref"} & default @{ML false} \\ @{index_ML unique_names: "bool Unsynchronized.ref"} & default @{ML true} \\ @@ -141,6 +142,8 @@ Note that the output can be enormous, because polymorphic constants often occur at several different type instances. + \item @{ML show_abbrevs} controls folding of constant abbreviations. + \item @{ML long_names}, @{ML short_names}, and @{ML unique_names} control the way of printing fully qualified internal names in external form. See also \secref{sec:antiq} for the document diff -r 7695e4de4d86 -r ca132ef44944 doc-src/IsarRef/Thy/document/Document_Preparation.tex --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Thu Dec 02 16:04:22 2010 +0100 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Thu Dec 02 16:52:52 2010 +0100 @@ -357,6 +357,9 @@ \item \indexdef{}{antiquotation option}{show\_structs}\hypertarget{antiquotation option.show-structs}{\hyperlink{antiquotation option.show-structs}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}structs}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} controls printing of implicit structures. + \item \indexdef{}{antiquotation option}{show\_abbrevs}\hypertarget{antiquotation option.show-abbrevs}{\hyperlink{antiquotation option.show-abbrevs}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}abbrevs}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} + controls folding of abbreviations. + \item \indexdef{}{antiquotation option}{long\_names}\hypertarget{antiquotation option.long-names}{\hyperlink{antiquotation option.long-names}{\mbox{\isa{long{\isaliteral{5F}{\isacharunderscore}}names}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} forces names of types and constants etc.\ to be printed in their fully qualified internal form. diff -r 7695e4de4d86 -r ca132ef44944 doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Thu Dec 02 16:04:22 2010 +0100 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Thu Dec 02 16:52:52 2010 +0100 @@ -121,6 +121,7 @@ \indexdef{}{ML}{show\_types}\verb|show_types: bool Config.T| & default \verb|false| \\ \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Config.T| & default \verb|false| \\ \indexdef{}{ML}{show\_consts}\verb|show_consts: bool Config.T| & default \verb|false| \\ + \indexdef{}{ML}{show\_abbrevs}\verb|show_abbrevs: bool Config.T| & default \verb|true| \\ \indexdef{}{ML}{long\_names}\verb|long_names: bool Unsynchronized.ref| & default \verb|false| \\ \indexdef{}{ML}{short\_names}\verb|short_names: bool Unsynchronized.ref| & default \verb|false| \\ \indexdef{}{ML}{unique\_names}\verb|unique_names: bool Unsynchronized.ref| & default \verb|true| \\ @@ -162,6 +163,8 @@ Note that the output can be enormous, because polymorphic constants often occur at several different type instances. + \item \verb|show_abbrevs| controls folding of constant abbreviations. + \item \verb|long_names|, \verb|short_names|, and \verb|unique_names| control the way of printing fully qualified internal names in external form. See also \secref{sec:antiq} for the document diff -r 7695e4de4d86 -r ca132ef44944 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Thu Dec 02 16:04:22 2010 +0100 +++ b/src/Pure/Isar/attrib.ML Thu Dec 02 16:52:52 2010 +0100 @@ -405,6 +405,7 @@ register_config Syntax.show_question_marks_raw #> register_config Syntax.ambiguity_level_raw #> register_config Syntax.eta_contract_raw #> + register_config ProofContext.show_abbrevs_raw #> register_config Goal_Display.goals_limit_raw #> register_config Goal_Display.show_main_goal_raw #> register_config Goal_Display.show_consts_raw #> diff -r 7695e4de4d86 -r ca132ef44944 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Dec 02 16:04:22 2010 +0100 +++ b/src/Pure/Isar/proof_context.ML Thu Dec 02 16:52:52 2010 +0100 @@ -70,6 +70,8 @@ val read_term_pattern: Proof.context -> string -> term val read_term_schematic: Proof.context -> string -> term val read_term_abbrev: Proof.context -> string -> term + val show_abbrevs_raw: Config.raw + val show_abbrevs: bool Config.T val expand_abbrevs: Proof.context -> term -> term val cert_term: Proof.context -> term -> term val cert_prop: Proof.context -> term -> term @@ -554,6 +556,8 @@ end; +val show_abbrevs_raw = Config.declare "show_abbrevs" (fn _ => Config.Bool true); +val show_abbrevs = Config.bool show_abbrevs_raw; fun contract_abbrevs ctxt t = let @@ -563,7 +567,7 @@ val retrieve = Consts.retrieve_abbrevs consts (print_mode_value () @ [""]); fun match_abbrev u = Option.map #1 (get_first (Pattern.match_rew thy u) (retrieve u)); in - if abbrev orelse print_mode_active "no_abbrevs" orelse not (can Term.type_of t) then t + if abbrev orelse not (Config.get ctxt show_abbrevs) orelse not (can Term.type_of t) then t else Pattern.rewrite_term_top thy [] [match_abbrev] t end; @@ -1480,3 +1484,5 @@ end; +val show_abbrevs = ProofContext.show_abbrevs; + diff -r 7695e4de4d86 -r ca132ef44944 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Thu Dec 02 16:04:22 2010 +0100 +++ b/src/Pure/Thy/thy_output.ML Thu Dec 02 16:52:52 2010 +0100 @@ -449,6 +449,7 @@ val _ = add_option "show_sorts" (Config.put show_sorts o boolean); val _ = add_option "show_structs" (Config.put show_structs o boolean); val _ = add_option "show_question_marks" (Config.put show_question_marks o boolean); +val _ = add_option "show_abbrevs" (Config.put show_abbrevs o boolean); val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean); val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean); val _ = add_option "unique_names" (add_wrapper o setmp_CRITICAL Name_Space.unique_names o boolean);