# HG changeset patch
# User wenzelm
# Date 1283505718 -7200
# Node ID 600de048585962141091c7094fbbe584413b7a88
# Parent  423b72f2d242ec05836ec522d00ba14caa53b3d6
turned show_consts into proper configuration option;

diff -r 423b72f2d242 -r 600de0485859 NEWS
--- a/NEWS	Fri Sep 03 10:58:11 2010 +0200
+++ b/NEWS	Fri Sep 03 11:21:58 2010 +0200
@@ -37,8 +37,9 @@
   Thy_Output.break          thy_output_break
 
   show_question_marks       show_question_marks
-
-Note that the corresponding "..._default" references may be only
+  show_consts               show_consts
+
+Note that the corresponding "..._default" references in ML may be only
 changed globally at the ROOT session setup, but *not* within a theory.
 
 
diff -r 423b72f2d242 -r 600de0485859 doc-src/IsarRef/Thy/Inner_Syntax.thy
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Fri Sep 03 10:58:11 2010 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Fri Sep 03 11:21:58 2010 +0200
@@ -98,7 +98,7 @@
   \begin{mldecls} 
     @{index_ML show_types: "bool Unsynchronized.ref"} & default @{ML false} \\
     @{index_ML show_sorts: "bool Unsynchronized.ref"} & default @{ML false} \\
-    @{index_ML show_consts: "bool Unsynchronized.ref"} & default @{ML false} \\
+    @{index_ML show_consts: "bool Config.T"} & default @{ML false} \\
     @{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} \\
diff -r 423b72f2d242 -r 600de0485859 doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Fri Sep 03 10:58:11 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Fri Sep 03 11:21:58 2010 +0200
@@ -120,7 +120,7 @@
 \begin{mldecls} 
     \indexdef{}{ML}{show\_types}\verb|show_types: bool Unsynchronized.ref| & default \verb|false| \\
     \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Unsynchronized.ref| & default \verb|false| \\
-    \indexdef{}{ML}{show\_consts}\verb|show_consts: bool Unsynchronized.ref| & default \verb|false| \\
+    \indexdef{}{ML}{show\_consts}\verb|show_consts: bool Config.T| & default \verb|false| \\
     \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| \\
diff -r 423b72f2d242 -r 600de0485859 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Fri Sep 03 10:58:11 2010 +0200
+++ b/src/HOL/Tools/refute.ML	Fri Sep 03 11:21:58 2010 +0200
@@ -268,8 +268,8 @@
         "Size of types: " ^ commas (map (fn (T, i) =>
           Syntax.string_of_typ ctxt T ^ ": " ^ string_of_int i) typs) ^ "\n"
     val show_consts_msg =
-      if not (!show_consts) andalso Library.exists (is_Const o fst) terms then
-        "set \"show_consts\" to show the interpretation of constants\n"
+      if not (Config.get ctxt show_consts) andalso Library.exists (is_Const o fst) terms then
+        "enable \"show_consts\" to show the interpretation of constants\n"
       else
         ""
     val terms_msg =
@@ -278,7 +278,7 @@
       else
         cat_lines (map_filter (fn (t, intr) =>
           (* print constants only if 'show_consts' is true *)
-          if (!show_consts) orelse not (is_Const t) then
+          if Config.get ctxt show_consts orelse not (is_Const t) then
             SOME (Syntax.string_of_term ctxt t ^ ": " ^
               Syntax.string_of_term ctxt
                 (print ctxt model (Term.type_of t) intr assignment))
diff -r 423b72f2d242 -r 600de0485859 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Sep 03 10:58:11 2010 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Sep 03 11:21:58 2010 +0200
@@ -392,7 +392,8 @@
 (* theory setup *)
 
 val _ = Context.>> (Context.map_theory
- (register_config show_question_marks_value #>
+ (register_config Syntax.show_question_marks_value #>
+  register_config Goal_Display.show_consts_value #>
   register_config Unify.trace_bound_value #>
   register_config Unify.search_bound_value #>
   register_config Unify.trace_simp_value #>
diff -r 423b72f2d242 -r 600de0485859 src/Pure/ProofGeneral/preferences.ML
--- a/src/Pure/ProofGeneral/preferences.ML	Fri Sep 03 10:58:11 2010 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Fri Sep 03 11:21:58 2010 +0200
@@ -117,7 +117,7 @@
   bool_pref show_sorts
     "show-sorts"
     "Include sorts in display of Isabelle terms",
-  bool_pref show_consts
+  bool_pref show_consts_default
     "show-consts"
     "Show types of consts in Isabelle goal display",
   bool_pref long_names
diff -r 423b72f2d242 -r 600de0485859 src/Pure/display.ML
--- a/src/Pure/display.ML	Fri Sep 03 10:58:11 2010 +0200
+++ b/src/Pure/display.ML	Fri Sep 03 11:21:58 2010 +0200
@@ -8,7 +8,8 @@
 signature BASIC_DISPLAY =
 sig
   val goals_limit: int Unsynchronized.ref
-  val show_consts: bool Unsynchronized.ref
+  val show_consts_default: bool Unsynchronized.ref
+  val show_consts: bool Config.T
   val show_hyps: bool Unsynchronized.ref
   val show_tags: bool Unsynchronized.ref
 end;
@@ -37,6 +38,7 @@
 (** options **)
 
 val goals_limit = Goal_Display.goals_limit;
+val show_consts_default = Goal_Display.show_consts_default;
 val show_consts = Goal_Display.show_consts;
 
 val show_hyps = Unsynchronized.ref false;    (*false: print meta-hypotheses as dots*)
diff -r 423b72f2d242 -r 600de0485859 src/Pure/goal_display.ML
--- a/src/Pure/goal_display.ML	Fri Sep 03 10:58:11 2010 +0200
+++ b/src/Pure/goal_display.ML	Fri Sep 03 11:21:58 2010 +0200
@@ -8,7 +8,9 @@
 signature GOAL_DISPLAY =
 sig
   val goals_limit: int Unsynchronized.ref
-  val show_consts: bool Unsynchronized.ref
+  val show_consts_default: bool Unsynchronized.ref
+  val show_consts_value: Config.value Config.T
+  val show_consts: bool Config.T
   val pretty_flexpair: Proof.context -> term * term -> Pretty.T
   val pretty_goals: Proof.context -> {total: bool, main: bool, maxgoals: int} ->
     thm -> Pretty.T list
@@ -19,7 +21,12 @@
 struct
 
 val goals_limit = Unsynchronized.ref 10;     (*max number of goals to print*)
-val show_consts = Unsynchronized.ref false;  (*true: show consts with types in proof state output*)
+
+(*true: show consts with types in proof state output*)
+val show_consts_default = Unsynchronized.ref false;
+val show_consts_value =
+  Config.declare false "show_consts" (fn _ => Config.Bool (! show_consts_default));
+val show_consts = Config.bool show_consts_value;
 
 fun pretty_flexpair ctxt (t, u) = Pretty.block
   [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
@@ -104,7 +111,7 @@
            else [])
         else pretty_subgoals As) @
       pretty_ffpairs tpairs @
-      (if ! show_consts then pretty_consts prop else []) @
+      (if Config.get ctxt show_consts then pretty_consts prop else []) @
       (if types then pretty_vars prop else []) @
       (if sorts then pretty_varsT prop else []);
   in