src/Pure/goal_display.ML
changeset 39050 600de0485859
parent 33957 e9afca2118d4
child 39115 a00da1674c1c
     1.1 --- a/src/Pure/goal_display.ML	Fri Sep 03 10:58:11 2010 +0200
     1.2 +++ b/src/Pure/goal_display.ML	Fri Sep 03 11:21:58 2010 +0200
     1.3 @@ -8,7 +8,9 @@
     1.4  signature GOAL_DISPLAY =
     1.5  sig
     1.6    val goals_limit: int Unsynchronized.ref
     1.7 -  val show_consts: bool Unsynchronized.ref
     1.8 +  val show_consts_default: bool Unsynchronized.ref
     1.9 +  val show_consts_value: Config.value Config.T
    1.10 +  val show_consts: bool Config.T
    1.11    val pretty_flexpair: Proof.context -> term * term -> Pretty.T
    1.12    val pretty_goals: Proof.context -> {total: bool, main: bool, maxgoals: int} ->
    1.13      thm -> Pretty.T list
    1.14 @@ -19,7 +21,12 @@
    1.15  struct
    1.16  
    1.17  val goals_limit = Unsynchronized.ref 10;     (*max number of goals to print*)
    1.18 -val show_consts = Unsynchronized.ref false;  (*true: show consts with types in proof state output*)
    1.19 +
    1.20 +(*true: show consts with types in proof state output*)
    1.21 +val show_consts_default = Unsynchronized.ref false;
    1.22 +val show_consts_value =
    1.23 +  Config.declare false "show_consts" (fn _ => Config.Bool (! show_consts_default));
    1.24 +val show_consts = Config.bool show_consts_value;
    1.25  
    1.26  fun pretty_flexpair ctxt (t, u) = Pretty.block
    1.27    [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
    1.28 @@ -104,7 +111,7 @@
    1.29             else [])
    1.30          else pretty_subgoals As) @
    1.31        pretty_ffpairs tpairs @
    1.32 -      (if ! show_consts then pretty_consts prop else []) @
    1.33 +      (if Config.get ctxt show_consts then pretty_consts prop else []) @
    1.34        (if types then pretty_vars prop else []) @
    1.35        (if sorts then pretty_varsT prop else []);
    1.36    in