configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;

--- 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.

--- 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.

--- 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

--- 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.

--- 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

--- 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 #>

--- 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;
+

--- 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);