1.1 --- a/NEWS	Thu Dec 02 16:04:22 2010 +0100
     1.2 +++ b/NEWS	Thu Dec 02 16:52:52 2010 +0100
     1.3 @@ -34,8 +34,8 @@
     1.4  
     1.5  * Various options that affect pretty printing etc. are now properly
     1.6  handled within the context via configuration options, instead of
     1.7 -unsynchronized references.  There are both ML Config.T entities and
     1.8 -Isar declaration attributes to access these.
     1.9 +unsynchronized references or print modes.  There are both ML Config.T
    1.10 +entities and Isar declaration attributes to access these.
    1.11  
    1.12    ML (Config.T)                 Isar (attribute)
    1.13  
    1.14 @@ -45,6 +45,7 @@
    1.15    show_types                    show_types
    1.16    show_question_marks           show_question_marks
    1.17    show_consts                   show_consts
    1.18 +  show_abbrevs                  show_abbrevs
    1.19  
    1.20    Syntax.ambiguity_level        syntax_ambiguity_level
    1.21  
    1.22 @@ -59,6 +60,8 @@
    1.23  
    1.24  Note that corresponding "..._default" references in ML may be only
    1.25  changed globally at the ROOT session setup, but *not* within a theory.
    1.26 +The option "show_abbrevs" supersedes the former print mode
    1.27 +"no_abbrevs" with inverted meaning.
    1.28  
    1.29  * More systematic naming of some configuration options.
    1.30    INCOMPATIBILTY.

     2.1 --- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Thu Dec 02 16:04:22 2010 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Thu Dec 02 16:52:52 2010 +0100
     2.3 @@ -339,6 +339,9 @@
     2.4    \item @{antiquotation_option_def show_structs}~@{text "= bool"}
     2.5    controls printing of implicit structures.
     2.6  
     2.7 +  \item @{antiquotation_option_def show_abbrevs}~@{text "= bool"}
     2.8 +  controls folding of abbreviations.
     2.9 +
    2.10    \item @{antiquotation_option_def long_names}~@{text "= bool"} forces
    2.11    names of types and constants etc.\ to be printed in their fully
    2.12    qualified internal form.

     3.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Dec 02 16:04:22 2010 +0100
     3.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Dec 02 16:52:52 2010 +0100
     3.3 @@ -99,6 +99,7 @@
     3.4      @{index_ML show_types: "bool Config.T"} & default @{ML false} \\
     3.5      @{index_ML show_sorts: "bool Config.T"} & default @{ML false} \\
     3.6      @{index_ML show_consts: "bool Config.T"} & default @{ML false} \\
     3.7 +    @{index_ML show_abbrevs: "bool Config.T"} & default @{ML true} \\
     3.8      @{index_ML long_names: "bool Unsynchronized.ref"} & default @{ML false} \\
     3.9      @{index_ML short_names: "bool Unsynchronized.ref"} & default @{ML false} \\
    3.10      @{index_ML unique_names: "bool Unsynchronized.ref"} & default @{ML true} \\
    3.11 @@ -141,6 +142,8 @@
    3.12    Note that the output can be enormous, because polymorphic constants
    3.13    often occur at several different type instances.
    3.14  
    3.15 +  \item @{ML show_abbrevs} controls folding of constant abbreviations.
    3.16 +
    3.17    \item @{ML long_names}, @{ML short_names}, and @{ML unique_names}
    3.18    control the way of printing fully qualified internal names in
    3.19    external form.  See also \secref{sec:antiq} for the document

     4.1 --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Thu Dec 02 16:04:22 2010 +0100
     4.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Thu Dec 02 16:52:52 2010 +0100
     4.3 @@ -357,6 +357,9 @@
     4.4    \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}}}
     4.5    controls printing of implicit structures.
     4.6  
     4.7 +  \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}}}
     4.8 +  controls folding of abbreviations.
     4.9 +
    4.10    \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
    4.11    names of types and constants etc.\ to be printed in their fully
    4.12    qualified internal form.

     5.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu Dec 02 16:04:22 2010 +0100
     5.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu Dec 02 16:52:52 2010 +0100
     5.3 @@ -121,6 +121,7 @@
     5.4      \indexdef{}{ML}{show\_types}\verb|show_types: bool Config.T| & default \verb|false| \\
     5.5      \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Config.T| & default \verb|false| \\
     5.6      \indexdef{}{ML}{show\_consts}\verb|show_consts: bool Config.T| & default \verb|false| \\
     5.7 +    \indexdef{}{ML}{show\_abbrevs}\verb|show_abbrevs: bool Config.T| & default \verb|true| \\
     5.8      \indexdef{}{ML}{long\_names}\verb|long_names: bool Unsynchronized.ref| & default \verb|false| \\
     5.9      \indexdef{}{ML}{short\_names}\verb|short_names: bool Unsynchronized.ref| & default \verb|false| \\
    5.10      \indexdef{}{ML}{unique\_names}\verb|unique_names: bool Unsynchronized.ref| & default \verb|true| \\
    5.11 @@ -162,6 +163,8 @@
    5.12    Note that the output can be enormous, because polymorphic constants
    5.13    often occur at several different type instances.
    5.14  
    5.15 +  \item \verb|show_abbrevs| controls folding of constant abbreviations.
    5.16 +
    5.17    \item \verb|long_names|, \verb|short_names|, and \verb|unique_names|
    5.18    control the way of printing fully qualified internal names in
    5.19    external form.  See also \secref{sec:antiq} for the document

     6.1 --- a/src/Pure/Isar/attrib.ML	Thu Dec 02 16:04:22 2010 +0100
     6.2 +++ b/src/Pure/Isar/attrib.ML	Thu Dec 02 16:52:52 2010 +0100
     6.3 @@ -405,6 +405,7 @@
     6.4    register_config Syntax.show_question_marks_raw #>
     6.5    register_config Syntax.ambiguity_level_raw #>
     6.6    register_config Syntax.eta_contract_raw #>
     6.7 +  register_config ProofContext.show_abbrevs_raw #>
     6.8    register_config Goal_Display.goals_limit_raw #>
     6.9    register_config Goal_Display.show_main_goal_raw #>
    6.10    register_config Goal_Display.show_consts_raw #>

     7.1 --- a/src/Pure/Isar/proof_context.ML	Thu Dec 02 16:04:22 2010 +0100
     7.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Dec 02 16:52:52 2010 +0100
     7.3 @@ -70,6 +70,8 @@
     7.4    val read_term_pattern: Proof.context -> string -> term
     7.5    val read_term_schematic: Proof.context -> string -> term
     7.6    val read_term_abbrev: Proof.context -> string -> term
     7.7 +  val show_abbrevs_raw: Config.raw
     7.8 +  val show_abbrevs: bool Config.T
     7.9    val expand_abbrevs: Proof.context -> term -> term
    7.10    val cert_term: Proof.context -> term -> term
    7.11    val cert_prop: Proof.context -> term -> term
    7.12 @@ -554,6 +556,8 @@
    7.13  
    7.14  end;
    7.15  
    7.16 +val show_abbrevs_raw = Config.declare "show_abbrevs" (fn _ => Config.Bool true);
    7.17 +val show_abbrevs = Config.bool show_abbrevs_raw;
    7.18  
    7.19  fun contract_abbrevs ctxt t =
    7.20    let
    7.21 @@ -563,7 +567,7 @@
    7.22      val retrieve = Consts.retrieve_abbrevs consts (print_mode_value () @ [""]);
    7.23      fun match_abbrev u = Option.map #1 (get_first (Pattern.match_rew thy u) (retrieve u));
    7.24    in
    7.25 -    if abbrev orelse print_mode_active "no_abbrevs" orelse not (can Term.type_of t) then t
    7.26 +    if abbrev orelse not (Config.get ctxt show_abbrevs) orelse not (can Term.type_of t) then t
    7.27      else Pattern.rewrite_term_top thy [] [match_abbrev] t
    7.28    end;
    7.29  
    7.30 @@ -1480,3 +1484,5 @@
    7.31  
    7.32  end;
    7.33  
    7.34 +val show_abbrevs = ProofContext.show_abbrevs;
    7.35 +

     8.1 --- a/src/Pure/Thy/thy_output.ML	Thu Dec 02 16:04:22 2010 +0100
     8.2 +++ b/src/Pure/Thy/thy_output.ML	Thu Dec 02 16:52:52 2010 +0100
     8.3 @@ -449,6 +449,7 @@
     8.4  val _ = add_option "show_sorts" (Config.put show_sorts o boolean);
     8.5  val _ = add_option "show_structs" (Config.put show_structs o boolean);
     8.6  val _ = add_option "show_question_marks" (Config.put show_question_marks o boolean);
     8.7 +val _ = add_option "show_abbrevs" (Config.put show_abbrevs o boolean);
     8.8  val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean);
     8.9  val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean);
    8.10  val _ = add_option "unique_names" (add_wrapper o setmp_CRITICAL Name_Space.unique_names o boolean);