--- 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.
--- 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} \\
--- 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| \\
--- 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))
--- 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 #>
--- 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
--- 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*)
--- 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