1.1 --- a/NEWS	Fri Sep 03 10:58:11 2010 +0200
     1.2 +++ b/NEWS	Fri Sep 03 11:21:58 2010 +0200
     1.3 @@ -37,8 +37,9 @@
     1.4    Thy_Output.break          thy_output_break
     1.5  
     1.6    show_question_marks       show_question_marks
     1.7 -
     1.8 -Note that the corresponding "..._default" references may be only
     1.9 +  show_consts               show_consts
    1.10 +
    1.11 +Note that the corresponding "..._default" references in ML may be only
    1.12  changed globally at the ROOT session setup, but *not* within a theory.
    1.13  
    1.14  

     2.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Fri Sep 03 10:58:11 2010 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Fri Sep 03 11:21:58 2010 +0200
     2.3 @@ -98,7 +98,7 @@
     2.4    \begin{mldecls} 
     2.5      @{index_ML show_types: "bool Unsynchronized.ref"} & default @{ML false} \\
     2.6      @{index_ML show_sorts: "bool Unsynchronized.ref"} & default @{ML false} \\
     2.7 -    @{index_ML show_consts: "bool Unsynchronized.ref"} & default @{ML false} \\
     2.8 +    @{index_ML show_consts: "bool Config.T"} & default @{ML false} \\
     2.9      @{index_ML long_names: "bool Unsynchronized.ref"} & default @{ML false} \\
    2.10      @{index_ML short_names: "bool Unsynchronized.ref"} & default @{ML false} \\
    2.11      @{index_ML unique_names: "bool Unsynchronized.ref"} & default @{ML true} \\

     3.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Fri Sep 03 10:58:11 2010 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Fri Sep 03 11:21:58 2010 +0200
     3.3 @@ -120,7 +120,7 @@
     3.4  \begin{mldecls} 
     3.5      \indexdef{}{ML}{show\_types}\verb|show_types: bool Unsynchronized.ref| & default \verb|false| \\
     3.6      \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Unsynchronized.ref| & default \verb|false| \\
     3.7 -    \indexdef{}{ML}{show\_consts}\verb|show_consts: bool Unsynchronized.ref| & default \verb|false| \\
     3.8 +    \indexdef{}{ML}{show\_consts}\verb|show_consts: bool Config.T| & default \verb|false| \\
     3.9      \indexdef{}{ML}{long\_names}\verb|long_names: bool Unsynchronized.ref| & default \verb|false| \\
    3.10      \indexdef{}{ML}{short\_names}\verb|short_names: bool Unsynchronized.ref| & default \verb|false| \\
    3.11      \indexdef{}{ML}{unique\_names}\verb|unique_names: bool Unsynchronized.ref| & default \verb|true| \\

     4.1 --- a/src/HOL/Tools/refute.ML	Fri Sep 03 10:58:11 2010 +0200
     4.2 +++ b/src/HOL/Tools/refute.ML	Fri Sep 03 11:21:58 2010 +0200
     4.3 @@ -268,8 +268,8 @@
     4.4          "Size of types: " ^ commas (map (fn (T, i) =>
     4.5            Syntax.string_of_typ ctxt T ^ ": " ^ string_of_int i) typs) ^ "\n"
     4.6      val show_consts_msg =
     4.7 -      if not (!show_consts) andalso Library.exists (is_Const o fst) terms then
     4.8 -        "set \"show_consts\" to show the interpretation of constants\n"
     4.9 +      if not (Config.get ctxt show_consts) andalso Library.exists (is_Const o fst) terms then
    4.10 +        "enable \"show_consts\" to show the interpretation of constants\n"
    4.11        else
    4.12          ""
    4.13      val terms_msg =
    4.14 @@ -278,7 +278,7 @@
    4.15        else
    4.16          cat_lines (map_filter (fn (t, intr) =>
    4.17            (* print constants only if 'show_consts' is true *)
    4.18 -          if (!show_consts) orelse not (is_Const t) then
    4.19 +          if Config.get ctxt show_consts orelse not (is_Const t) then
    4.20              SOME (Syntax.string_of_term ctxt t ^ ": " ^
    4.21                Syntax.string_of_term ctxt
    4.22                  (print ctxt model (Term.type_of t) intr assignment))

     5.1 --- a/src/Pure/Isar/attrib.ML	Fri Sep 03 10:58:11 2010 +0200
     5.2 +++ b/src/Pure/Isar/attrib.ML	Fri Sep 03 11:21:58 2010 +0200
     5.3 @@ -392,7 +392,8 @@
     5.4  (* theory setup *)
     5.5  
     5.6  val _ = Context.>> (Context.map_theory
     5.7 - (register_config show_question_marks_value #>
     5.8 + (register_config Syntax.show_question_marks_value #>
     5.9 +  register_config Goal_Display.show_consts_value #>
    5.10    register_config Unify.trace_bound_value #>
    5.11    register_config Unify.search_bound_value #>
    5.12    register_config Unify.trace_simp_value #>

     6.1 --- a/src/Pure/ProofGeneral/preferences.ML	Fri Sep 03 10:58:11 2010 +0200
     6.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Fri Sep 03 11:21:58 2010 +0200
     6.3 @@ -117,7 +117,7 @@
     6.4    bool_pref show_sorts
     6.5      "show-sorts"
     6.6      "Include sorts in display of Isabelle terms",
     6.7 -  bool_pref show_consts
     6.8 +  bool_pref show_consts_default
     6.9      "show-consts"
    6.10      "Show types of consts in Isabelle goal display",
    6.11    bool_pref long_names

     7.1 --- a/src/Pure/display.ML	Fri Sep 03 10:58:11 2010 +0200
     7.2 +++ b/src/Pure/display.ML	Fri Sep 03 11:21:58 2010 +0200
     7.3 @@ -8,7 +8,8 @@
     7.4  signature BASIC_DISPLAY =
     7.5  sig
     7.6    val goals_limit: int Unsynchronized.ref
     7.7 -  val show_consts: bool Unsynchronized.ref
     7.8 +  val show_consts_default: bool Unsynchronized.ref
     7.9 +  val show_consts: bool Config.T
    7.10    val show_hyps: bool Unsynchronized.ref
    7.11    val show_tags: bool Unsynchronized.ref
    7.12  end;
    7.13 @@ -37,6 +38,7 @@
    7.14  (** options **)
    7.15  
    7.16  val goals_limit = Goal_Display.goals_limit;
    7.17 +val show_consts_default = Goal_Display.show_consts_default;
    7.18  val show_consts = Goal_Display.show_consts;
    7.19  
    7.20  val show_hyps = Unsynchronized.ref false;    (*false: print meta-hypotheses as dots*)

     8.1 --- a/src/Pure/goal_display.ML	Fri Sep 03 10:58:11 2010 +0200
     8.2 +++ b/src/Pure/goal_display.ML	Fri Sep 03 11:21:58 2010 +0200
     8.3 @@ -8,7 +8,9 @@
     8.4  signature GOAL_DISPLAY =
     8.5  sig
     8.6    val goals_limit: int Unsynchronized.ref
     8.7 -  val show_consts: bool Unsynchronized.ref
     8.8 +  val show_consts_default: bool Unsynchronized.ref
     8.9 +  val show_consts_value: Config.value Config.T
    8.10 +  val show_consts: bool Config.T
    8.11    val pretty_flexpair: Proof.context -> term * term -> Pretty.T
    8.12    val pretty_goals: Proof.context -> {total: bool, main: bool, maxgoals: int} ->
    8.13      thm -> Pretty.T list
    8.14 @@ -19,7 +21,12 @@
    8.15  struct
    8.16  
    8.17  val goals_limit = Unsynchronized.ref 10;     (*max number of goals to print*)
    8.18 -val show_consts = Unsynchronized.ref false;  (*true: show consts with types in proof state output*)
    8.19 +
    8.20 +(*true: show consts with types in proof state output*)
    8.21 +val show_consts_default = Unsynchronized.ref false;
    8.22 +val show_consts_value =
    8.23 +  Config.declare false "show_consts" (fn _ => Config.Bool (! show_consts_default));
    8.24 +val show_consts = Config.bool show_consts_value;
    8.25  
    8.26  fun pretty_flexpair ctxt (t, u) = Pretty.block
    8.27    [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
    8.28 @@ -104,7 +111,7 @@
    8.29             else [])
    8.30          else pretty_subgoals As) @
    8.31        pretty_ffpairs tpairs @
    8.32 -      (if ! show_consts then pretty_consts prop else []) @
    8.33 +      (if Config.get ctxt show_consts then pretty_consts prop else []) @
    8.34        (if types then pretty_vars prop else []) @
    8.35        (if sorts then pretty_varsT prop else []);
    8.36    in