clarified message when subgoals have been stripped -- unconditional;
authorwenzelm
Mon May 13 13:01:10 2013 +0200 (2013-05-13)
changeset 5195918d758e38d85
parent 51958 bca32217b304
child 51960 61ac1efe02c3
clarified message when subgoals have been stripped -- unconditional;
src/Pure/goal_display.ML
     1.1 --- a/src/Pure/goal_display.ML	Mon May 13 12:40:17 2013 +0200
     1.2 +++ b/src/Pure/goal_display.ML	Mon May 13 13:01:10 2013 +0200
     1.3 @@ -10,7 +10,6 @@
     1.4    val goals_limit_default: int Unsynchronized.ref
     1.5    val goals_limit_raw: Config.raw
     1.6    val goals_limit: int Config.T
     1.7 -  val goals_total: bool Config.T
     1.8    val show_main_goal_default: bool Unsynchronized.ref
     1.9    val show_main_goal_raw: Config.raw
    1.10    val show_main_goal: bool Config.T
    1.11 @@ -31,8 +30,6 @@
    1.12  val goals_limit_raw = Config.declare "goals_limit" (fn _ => Config.Int (! goals_limit_default));
    1.13  val goals_limit = Config.int goals_limit_raw;
    1.14  
    1.15 -val goals_total = Config.bool (Config.declare "goals_total" (fn _ => Config.Bool true));
    1.16 -
    1.17  val show_main_goal_default = Unsynchronized.ref false;
    1.18  val show_main_goal_raw =
    1.19    Config.declare "show_main_goal" (fn _ => Config.Bool (! show_main_goal_default));
    1.20 @@ -92,7 +89,6 @@
    1.21      val show_consts = Config.get ctxt show_consts
    1.22      val show_main_goal = Config.get ctxt show_main_goal;
    1.23      val goals_limit = Config.get ctxt goals_limit;
    1.24 -    val goals_total = Config.get ctxt goals_total;
    1.25  
    1.26      val prt_sort = Syntax.pretty_sort ctxt;
    1.27      val prt_typ = Syntax.pretty_typ ctxt;
    1.28 @@ -135,8 +131,7 @@
    1.29       (if ngoals = 0 then [Pretty.str "No subgoals!"]
    1.30        else if ngoals > goals_limit then
    1.31          pretty_subgoals (take goals_limit As) @
    1.32 -        (if goals_total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
    1.33 -         else [])
    1.34 +        [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
    1.35        else pretty_subgoals As) @
    1.36      pretty_ffpairs tpairs @
    1.37      (if show_consts then pretty_consts prop else []) @
    1.38 @@ -149,9 +144,7 @@
    1.39      Config.put show_main_goal true (Syntax.init_pretty_global (Thm.theory_of_thm th))
    1.40    in pretty_goals ctxt th end;
    1.41  
    1.42 -fun pretty_goal ctxt th =
    1.43 -  Pretty.chunks (pretty_goals (Config.put goals_total false ctxt) th);
    1.44 -
    1.45 +val pretty_goal = Pretty.chunks oo pretty_goals;
    1.46  val string_of_goal = Pretty.string_of oo pretty_goal;
    1.47  
    1.48  end;