src/Pure/goal_display.ML
changeset 39125 f45d332a90e3
parent 39118 12f3788be67b
child 39134 917b4b6ba3d2
--- a/src/Pure/goal_display.ML	Fri Sep 03 20:39:38 2010 +0200
+++ b/src/Pure/goal_display.ML	Fri Sep 03 21:13:53 2010 +0200
@@ -7,22 +7,35 @@
 
 signature GOAL_DISPLAY =
 sig
-  val goals_limit: int Unsynchronized.ref
+  val goals_limit_default: int Unsynchronized.ref
+  val goals_limit_value: Config.value Config.T
+  val goals_limit: int Config.T
+  val goals_total: bool Config.T
+  val show_main_goal_default: bool Unsynchronized.ref
+  val show_main_goal_value: Config.value Config.T
+  val show_main_goal: bool Config.T
   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
-  val pretty_goals_without_context: int -> thm -> Pretty.T list
+  val pretty_goals: Proof.context -> thm -> Pretty.T list
+  val pretty_goals_without_context: thm -> Pretty.T list
 end;
 
 structure Goal_Display: GOAL_DISPLAY =
 struct
 
-val goals_limit = Unsynchronized.ref 10;     (*max number of goals to print*)
+val goals_limit_default = Unsynchronized.ref 10;
+val goals_limit_value = Config.declare "goals_limit" (fn _ => Config.Int (! goals_limit_default));
+val goals_limit = Config.int goals_limit_value;
+
+val goals_total = Config.bool (Config.declare "goals_total" (fn _ => Config.Bool true));
 
-(*true: show consts with types in proof state output*)
+val show_main_goal_default = Unsynchronized.ref false;
+val show_main_goal_value =
+  Config.declare "show_main_goal" (fn _ => Config.Bool (! show_main_goal_default));
+val show_main_goal = Config.bool show_main_goal_value;
+
 val show_consts_default = Unsynchronized.ref false;
 val show_consts_value = Config.declare "show_consts" (fn _ => Config.Bool (! show_consts_default));
 val show_consts = Config.bool show_consts_value;
@@ -62,10 +75,14 @@
 
 in
 
-fun pretty_goals ctxt0 {total, main, maxgoals} state =
+fun pretty_goals ctxt0 state =
   let
     val ctxt = Config.put show_free_types false ctxt0;
+
     val show_all_types = Config.get ctxt show_all_types;
+    val goals_limit = Config.get ctxt goals_limit;
+    val goals_total = Config.get ctxt goals_total;
+    val show_main_goal = Config.get ctxt show_main_goal;
 
     val prt_sort = Syntax.pretty_sort ctxt;
     val prt_typ = Syntax.pretty_typ ctxt;
@@ -105,11 +122,11 @@
     val ngoals = length As;
 
     fun pretty_gs (types, sorts) =
-      (if main then [prt_term B] else []) @
+      (if show_main_goal then [prt_term B] else []) @
        (if ngoals = 0 then [Pretty.str "No subgoals!"]
-        else if ngoals > maxgoals then
-          pretty_subgoals (take maxgoals As) @
-          (if total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
+        else if ngoals > goals_limit then
+          pretty_subgoals (take goals_limit As) @
+          (if goals_total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
            else [])
         else pretty_subgoals As) @
       pretty_ffpairs tpairs @
@@ -122,9 +139,10 @@
    (! show_types orelse ! show_sorts orelse show_all_types, ! show_sorts)
   end;
 
-fun pretty_goals_without_context n th =
-  pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm th))
-    {total = true, main = true, maxgoals = n} th;
+fun pretty_goals_without_context th =
+  let val ctxt =
+    Config.put show_main_goal true (Syntax.init_pretty_global (Thm.theory_of_thm th))
+  in pretty_goals ctxt th end;
 
 end;