pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;

--- a/NEWS	Fri Sep 03 20:39:38 2010 +0200
+++ b/NEWS	Fri Sep 03 21:13:53 2010 +0200
@@ -28,18 +28,21 @@
 unsynchronized references.  There are both ML Config.T entities and
 Isar declaration attributes to access these.
 
-  ML:                       Isar:
-
-  Thy_Output.display        thy_output_display
-  Thy_Output.quotes         thy_output_quotes
-  Thy_Output.indent         thy_output_indent
-  Thy_Output.source         thy_output_source
-  Thy_Output.break          thy_output_break
-
-  show_question_marks       show_question_marks
-  show_consts               show_consts
-
-Note that the corresponding "..._default" references in ML may be only
+  ML (Config.T)                 Isar (attribute)
+
+  Thy_Output.display            thy_output_display
+  Thy_Output.quotes             thy_output_quotes
+  Thy_Output.indent             thy_output_indent
+  Thy_Output.source             thy_output_source
+  Thy_Output.break              thy_output_break
+
+  show_question_marks           show_question_marks
+  show_consts                   show_consts
+
+  Goal_Display.goals_limit      goals_limit
+  Goal_Display.show_main_goal   show_main_goal
+
+Note that corresponding "..._default" references in ML may be only
 changed globally at the ROOT session setup, but *not* within a theory.
 
 

--- a/src/HOL/Prolog/prolog.ML	Fri Sep 03 20:39:38 2010 +0200
+++ b/src/HOL/Prolog/prolog.ML	Fri Sep 03 21:13:53 2010 +0200
@@ -2,7 +2,7 @@
     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
 *)
 
-Proof.show_main_goal := true;
+Goal_Display.show_main_goal_default := true;
 
 structure Prolog =
 struct

--- a/src/HOL/Tools/Function/lexicographic_order.ML	Fri Sep 03 20:39:38 2010 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Fri Sep 03 21:13:53 2010 +0200
@@ -135,7 +135,8 @@
 (** Error reporting **)
 
 fun pr_goals ctxt st =
-  Goal_Display.pretty_goals ctxt {total = true, main = false, maxgoals = Thm.nprems_of st} st
+  Goal_Display.pretty_goals
+    (Config.put Goal_Display.goals_limit (Thm.nprems_of st) ctxt) st
   |> Pretty.chunks
   |> Pretty.string_of
 

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Sep 03 20:39:38 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Sep 03 21:13:53 2010 +0200
@@ -97,7 +97,7 @@
   if (nprems_of st <= i) then Seq.single st
   else raise Fail ("assert_tac: Numbers of subgoals mismatch at goal state :"
     ^ "\n" ^ Pretty.string_of (Pretty.chunks
-      (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st)));
+      (Goal_Display.pretty_goals_without_context st)));
 
 (** fundamentals **)
 

--- a/src/Pure/Isar/attrib.ML	Fri Sep 03 20:39:38 2010 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Sep 03 21:13:53 2010 +0200
@@ -393,6 +393,8 @@
 
 val _ = Context.>> (Context.map_theory
  (register_config Syntax.show_question_marks_value #>
+  register_config Goal_Display.goals_limit_value #>
+  register_config Goal_Display.show_main_goal_value #>
   register_config Goal_Display.show_consts_value #>
   register_config Unify.trace_bound_value #>
   register_config Unify.search_bound_value #>

--- a/src/Pure/Isar/isar_cmd.ML	Fri Sep 03 20:39:38 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Sep 03 21:13:53 2010 +0200
@@ -272,8 +272,10 @@
   | set_limit r (SOME n) = r := n;
 
 fun pr (modes, (lim1, lim2)) = Toplevel.keep (fn state =>
-  (set_limit goals_limit lim1; set_limit ProofContext.prems_limit lim2; Toplevel.quiet := false;
-    Print_Mode.with_modes modes (Toplevel.print_state true) state));
+ (set_limit Goal_Display.goals_limit_default lim1;
+  set_limit ProofContext.prems_limit lim2;
+  Toplevel.quiet := false;
+  Print_Mode.with_modes modes (Toplevel.print_state true) state));
 
 val disable_pr = Toplevel.imperative (fn () => Toplevel.quiet := true);
 val enable_pr = Toplevel.imperative (fn () => Toplevel.quiet := false);

--- a/src/Pure/Isar/proof.ML	Fri Sep 03 20:39:38 2010 +0200
+++ b/src/Pure/Isar/proof.ML	Fri Sep 03 21:13:53 2010 +0200
@@ -30,7 +30,6 @@
   val assert_no_chain: state -> state
   val enter_forward: state -> state
   val goal_message: (unit -> Pretty.T) -> state -> state
-  val show_main_goal: bool Unsynchronized.ref
   val verbose: bool Unsynchronized.ref
   val pretty_state: int -> state -> Pretty.T list
   val pretty_goals: bool -> state -> Pretty.T list
@@ -322,7 +321,6 @@
 
 (** pretty_state **)
 
-val show_main_goal = Unsynchronized.ref false;
 val verbose = ProofContext.verbose;
 
 fun pretty_facts _ _ NONE = []
@@ -351,8 +349,7 @@
             (if mode <> Backward orelse null using then NONE else SOME using) @
           [Pretty.str ("goal" ^
             description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @
-          Goal_Display.pretty_goals ctxt
-            {total = true, main = ! show_main_goal, maxgoals = ! Display.goals_limit} goal @
+          Goal_Display.pretty_goals ctxt goal @
           (map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages))
       | prt_goal NONE = [];
 
@@ -372,10 +369,12 @@
   end;
 
 fun pretty_goals main state =
-  let val (ctxt, (_, goal)) = get_goal state in
-    Goal_Display.pretty_goals ctxt
-      {total = false, main = main, maxgoals = ! Display.goals_limit} goal
-  end;
+  let
+    val (ctxt, (_, goal)) = get_goal state;
+    val ctxt' = ctxt
+      |> Config.put Goal_Display.show_main_goal main
+      |> Config.put Goal_Display.goals_total false;
+  in Goal_Display.pretty_goals ctxt' goal end;
 
 
 
@@ -478,8 +477,7 @@
 
     val ngoals = Thm.nprems_of goal;
     val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks
-      (Goal_Display.pretty_goals ctxt
-          {total = true, main = ! show_main_goal, maxgoals = ! Display.goals_limit} goal @
+      (Goal_Display.pretty_goals ctxt goal @
         [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")])));
 
     val extra_hyps = Assumption.extra_hyps ctxt goal;

--- a/src/Pure/ProofGeneral/preferences.ML	Fri Sep 03 20:39:38 2010 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Fri Sep 03 21:13:53 2010 +0200
@@ -126,7 +126,7 @@
   bool_pref show_brackets
     "show-brackets"
     "Show full bracketing in Isabelle terms",
-  bool_pref Proof.show_main_goal
+  bool_pref Goal_Display.show_main_goal_default
     "show-main-goal"
     "Show main goal in proof state display",
   bool_pref Syntax.eta_contract
@@ -134,7 +134,7 @@
     "Print terms eta-contracted"];
 
 val advanced_display_preferences =
- [nat_pref goals_limit
+ [nat_pref Goal_Display.goals_limit_default
     "goals-limit"
     "Setting for maximum number of goals printed",
   int_pref ProofContext.prems_limit

--- a/src/Pure/Thy/thy_output.ML	Fri Sep 03 20:39:38 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML	Fri Sep 03 21:13:53 2010 +0200
@@ -459,7 +459,7 @@
 val _ = add_option "margin" (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer);
 val _ = add_option "indent" (Config.put indent o integer);
 val _ = add_option "source" (Config.put source o boolean);
-val _ = add_option "goals_limit" (add_wrapper o setmp_CRITICAL goals_limit o integer);
+val _ = add_option "goals_limit" (Config.put Goal_Display.goals_limit o integer);
 
 
 (* basic pretty printing *)
@@ -582,7 +582,7 @@
   | _ => error "No proof state");
 
 fun goal_state name main_goal = antiquotation name (Scan.succeed ())
-  (fn {state, context, ...} => fn () => output context
+  (fn {state, context = ctxt, ...} => fn () => output ctxt
     [Pretty.chunks (Proof.pretty_goals main_goal (proof_state state))]);
 
 in

--- a/src/Pure/display.ML	Fri Sep 03 20:39:38 2010 +0200
+++ b/src/Pure/display.ML	Fri Sep 03 21:13:53 2010 +0200
@@ -7,7 +7,6 @@
 
 signature BASIC_DISPLAY =
 sig
-  val goals_limit: int Unsynchronized.ref
   val show_consts_default: bool Unsynchronized.ref
   val show_consts: bool Config.T
   val show_hyps: bool Unsynchronized.ref
@@ -37,7 +36,6 @@
 
 (** options **)
 
-val goals_limit = Goal_Display.goals_limit;
 val show_consts_default = Goal_Display.show_consts_default;
 val show_consts = Goal_Display.show_consts;
 

--- a/src/Pure/goal.ML	Fri Sep 03 20:39:38 2010 +0200
+++ b/src/Pure/goal.ML	Fri Sep 03 21:13:53 2010 +0200
@@ -83,7 +83,10 @@
     0 => ()
   | n => raise THM ("Proof failed.\n" ^
       Pretty.string_of (Pretty.chunks
-        (Goal_Display.pretty_goals ctxt {total = true, main = true, maxgoals = n} th)) ^
+        (Goal_Display.pretty_goals
+          (ctxt
+            |> Config.put Goal_Display.goals_limit n
+            |> Config.put Goal_Display.show_main_goal true) th)) ^
       "\n" ^ string_of_int n ^ " unsolved goal(s)!", 0, [th]));
 
 fun finish ctxt th = (check_finished ctxt th; conclude th);

--- 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;
 

--- a/src/Pure/tactical.ML	Fri Sep 03 20:39:38 2010 +0200
+++ b/src/Pure/tactical.ML	Fri Sep 03 21:13:53 2010 +0200
@@ -191,8 +191,7 @@
 (*Print the current proof state and pass it on.*)
 fun print_tac msg st =
  (tracing (msg ^ "\n" ^
-    Pretty.string_of (Pretty.chunks
-      (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st)));
+    Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals_without_context st)));
   Seq.single st);
 
 (*Pause until a line is typed -- if non-empty then fail. *)
@@ -231,7 +230,7 @@
 fun tracify flag tac st =
   if !flag andalso not (!suppress_tracing) then
     (tracing (Pretty.string_of (Pretty.chunks
-        (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st @
+        (Goal_Display.pretty_goals_without_context st @
           [Pretty.str "** Press RETURN to continue:"])));
      exec_trace_command flag (tac, st))
   else tac st;