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;