--- a/src/HOL/Tools/Function/lexicographic_order.ML Sat Oct 13 18:04:11 2012 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Sat Oct 13 19:53:04 2012 +0200
@@ -122,10 +122,9 @@
(** Error reporting **)
fun pr_goals ctxt st =
- Goal_Display.pretty_goals
- (Config.put Goal_Display.goals_limit (Thm.nprems_of st) ctxt) st
- |> Pretty.chunks
- |> Pretty.string_of
+ Pretty.string_of
+ (Goal_Display.pretty_goal
+ {main = Config.get ctxt Goal_Display.show_main_goal, limit = false} ctxt st)
fun row_index i = chr (i + 97)
fun col_index j = string_of_int (j + 1)
--- a/src/Pure/Isar/proof.ML Sat Oct 13 18:04:11 2012 +0200
+++ b/src/Pure/Isar/proof.ML Sat Oct 13 19:53:04 2012 +0200
@@ -33,7 +33,6 @@
val enter_forward: state -> state
val goal_message: (unit -> Pretty.T) -> state -> state
val pretty_state: int -> state -> Pretty.T list
- val pretty_goals: bool -> state -> Pretty.T list
val refine: Method.text -> state -> state Seq.seq
val refine_end: Method.text -> state -> state Seq.seq
val refine_insert: thm list -> state -> state
@@ -378,14 +377,6 @@
else prt_goal (try find_goal state))
end;
-fun pretty_goals main state =
- let
- val (_, (_, goal)) = get_goal state;
- val ctxt = context_of state
- |> Config.put Goal_Display.show_main_goal main
- |> Config.put Goal_Display.goals_total false;
- in Goal_Display.pretty_goals ctxt goal end;
-
(** proof steps **)
@@ -490,18 +481,14 @@
(* conclude goal *)
-fun unfinished_goal_msg ctxt goal =
- Pretty.string_of (Pretty.chunks
- (Goal_Display.pretty_goals ctxt goal @
- [Pretty.str (string_of_int (Thm.nprems_of goal) ^ " unsolved goal(s)")]));
-
fun conclude_goal ctxt goal propss =
let
val thy = Proof_Context.theory_of ctxt;
val string_of_term = Syntax.string_of_term ctxt;
val string_of_thm = Display.string_of_thm ctxt;
- val _ = Thm.no_prems goal orelse error (unfinished_goal_msg ctxt goal);
+ val _ = Thm.no_prems goal orelse
+ error (Pretty.string_of (Goal_Display.pretty_goal {main = true, limit = false} ctxt goal));
val extra_hyps = Assumption.extra_hyps ctxt goal;
val _ = null extra_hyps orelse
@@ -535,7 +522,10 @@
else
(case Seq.pull (Seq.filter (Thm.no_prems o #2 o #2 o get_goal o #2) rest) of
SOME ((f, state), _) => f state
- | NONE => error ("Failed to finish proof:\n" ^ unfinished_goal_msg ctxt1 goal1))
+ | NONE =>
+ error ("Failed to finish proof:\n" ^
+ Pretty.string_of
+ (Goal_Display.pretty_goal {main = true, limit = false} ctxt1 goal1)))
end
| NONE => error "Failed to finish proof");
--- a/src/Pure/Thy/thy_output.ML Sat Oct 13 18:04:11 2012 +0200
+++ b/src/Pure/Thy/thy_output.ML Sat Oct 13 19:53:04 2012 +0200
@@ -609,14 +609,13 @@
local
fun proof_state state =
- (case try Toplevel.proof_of state of
- SOME prf => prf
+ (case try (Proof.goal o Toplevel.proof_of) state of
+ SOME {goal, ...} => goal
| _ => error "No proof state");
-fun goal_state name main_goal = antiquotation name (Scan.succeed ())
+fun goal_state name main = antiquotation name (Scan.succeed ())
(fn {state, context = ctxt, ...} => fn () => output ctxt
- [Pretty.chunks
- (Proof.pretty_goals main_goal (Proof.map_context (K ctxt) (proof_state state)))]);
+ [Goal_Display.pretty_goal {main = main, limit = true} ctxt (proof_state state)]);
in
--- a/src/Pure/goal.ML Sat Oct 13 18:04:11 2012 +0200
+++ b/src/Pure/goal.ML Sat Oct 13 19:53:04 2012 +0200
@@ -87,12 +87,7 @@
(case Thm.nprems_of th of
0 => th
| n => raise THM ("Proof failed.\n" ^
- Pretty.string_of (Pretty.chunks
- (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]));
+ Pretty.string_of (Goal_Display.pretty_goal {main = true, limit = false} ctxt th), 0, [th]));
fun finish ctxt = check_finished ctxt #> conclude;
--- a/src/Pure/goal_display.ML Sat Oct 13 18:04:11 2012 +0200
+++ b/src/Pure/goal_display.ML Sat Oct 13 19:53:04 2012 +0200
@@ -20,6 +20,7 @@
val pretty_flexpair: Proof.context -> term * term -> Pretty.T
val pretty_goals: Proof.context -> thm -> Pretty.T list
val pretty_goals_without_context: thm -> Pretty.T list
+ val pretty_goal: {main: bool, limit: bool} -> Proof.context -> thm -> Pretty.T
end;
structure Goal_Display: GOAL_DISPLAY =
@@ -148,6 +149,13 @@
Config.put show_main_goal true (Syntax.init_pretty_global (Thm.theory_of_thm th))
in pretty_goals ctxt th end;
+fun pretty_goal {main, limit} ctxt th =
+ Pretty.chunks (pretty_goals
+ (ctxt
+ |> Config.put show_main_goal main
+ |> not limit ? Config.put goals_limit (Thm.nprems_of th)
+ |> Config.put goals_total false) th);
+
end;
end;