src/Pure/goal_display.ML
changeset 39163 4d701c0388c3
parent 39134 917b4b6ba3d2
child 45666 d83797ef0d2d
     1.1 --- a/src/Pure/goal_display.ML	Mon Sep 06 19:23:54 2010 +0200
     1.2 +++ b/src/Pure/goal_display.ML	Mon Sep 06 21:33:19 2010 +0200
     1.3 @@ -8,14 +8,14 @@
     1.4  signature GOAL_DISPLAY =
     1.5  sig
     1.6    val goals_limit_default: int Unsynchronized.ref
     1.7 -  val goals_limit_value: Config.value Config.T
     1.8 +  val goals_limit_raw: Config.raw
     1.9    val goals_limit: int Config.T
    1.10    val goals_total: bool Config.T
    1.11    val show_main_goal_default: bool Unsynchronized.ref
    1.12 -  val show_main_goal_value: Config.value Config.T
    1.13 +  val show_main_goal_raw: Config.raw
    1.14    val show_main_goal: bool Config.T
    1.15    val show_consts_default: bool Unsynchronized.ref
    1.16 -  val show_consts_value: Config.value Config.T
    1.17 +  val show_consts_raw: Config.raw
    1.18    val show_consts: bool Config.T
    1.19    val pretty_flexpair: Proof.context -> term * term -> Pretty.T
    1.20    val pretty_goals: Proof.context -> thm -> Pretty.T list
    1.21 @@ -26,19 +26,19 @@
    1.22  struct
    1.23  
    1.24  val goals_limit_default = Unsynchronized.ref 10;
    1.25 -val goals_limit_value = Config.declare "goals_limit" (fn _ => Config.Int (! goals_limit_default));
    1.26 -val goals_limit = Config.int goals_limit_value;
    1.27 +val goals_limit_raw = Config.declare "goals_limit" (fn _ => Config.Int (! goals_limit_default));
    1.28 +val goals_limit = Config.int goals_limit_raw;
    1.29  
    1.30  val goals_total = Config.bool (Config.declare "goals_total" (fn _ => Config.Bool true));
    1.31  
    1.32  val show_main_goal_default = Unsynchronized.ref false;
    1.33 -val show_main_goal_value =
    1.34 +val show_main_goal_raw =
    1.35    Config.declare "show_main_goal" (fn _ => Config.Bool (! show_main_goal_default));
    1.36 -val show_main_goal = Config.bool show_main_goal_value;
    1.37 +val show_main_goal = Config.bool show_main_goal_raw;
    1.38  
    1.39  val show_consts_default = Unsynchronized.ref false;
    1.40 -val show_consts_value = Config.declare "show_consts" (fn _ => Config.Bool (! show_consts_default));
    1.41 -val show_consts = Config.bool show_consts_value;
    1.42 +val show_consts_raw = Config.declare "show_consts" (fn _ => Config.Bool (! show_consts_default));
    1.43 +val show_consts = Config.bool show_consts_raw;
    1.44  
    1.45  fun pretty_flexpair ctxt (t, u) = Pretty.block
    1.46    [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];