--- a/src/HOL/Tools/Function/lexicographic_order.ML Sat Jul 25 00:53:47 2009 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Sat Jul 25 10:31:27 2009 +0200
@@ -140,7 +140,7 @@
fun pr_table table = writeln (cat_lines (map (fn r => concat (map pr_cell r)) table))
fun pr_goals ctxt st =
- Display_Goal.pretty_goals ctxt {total = true, main = false, maxgoals = Thm.nprems_of st} st
+ Goal_Display.pretty_goals ctxt {total = true, main = false, maxgoals = Thm.nprems_of st} st
|> Pretty.chunks
|> Pretty.string_of
--- a/src/Pure/IsaMakefile Sat Jul 25 00:53:47 2009 +0200
+++ b/src/Pure/IsaMakefile Sat Jul 25 10:31:27 2009 +0200
@@ -90,7 +90,7 @@
Tools/find_theorems.ML Tools/named_thms.ML Tools/xml_syntax.ML \
assumption.ML axclass.ML codegen.ML config.ML conjunction.ML \
consts.ML context.ML context_position.ML conv.ML defs.ML display.ML \
- display_goal.ML drule.ML envir.ML facts.ML goal.ML interpretation.ML \
+ drule.ML envir.ML facts.ML goal.ML goal_display.ML interpretation.ML \
item_net.ML library.ML logic.ML meta_simplifier.ML more_thm.ML \
morphism.ML name.ML net.ML old_goals.ML old_term.ML pattern.ML \
primitive_defs.ML proofterm.ML pure_setup.ML pure_thy.ML search.ML \
--- a/src/Pure/Isar/proof.ML Sat Jul 25 00:53:47 2009 +0200
+++ b/src/Pure/Isar/proof.ML Sat Jul 25 10:31:27 2009 +0200
@@ -344,7 +344,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)] ^ ":")] @
- Display_Goal.pretty_goals ctxt
+ Goal_Display.pretty_goals ctxt
{total = true, main = ! show_main_goal, maxgoals = ! Display.goals_limit} goal @
(map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages))
| prt_goal NONE = [];
@@ -366,7 +366,7 @@
fun pretty_goals main state =
let val (ctxt, (_, goal)) = get_goal state in
- Display_Goal.pretty_goals ctxt
+ Goal_Display.pretty_goals ctxt
{total = false, main = main, maxgoals = ! Display.goals_limit} goal
end;
@@ -474,7 +474,7 @@
val ngoals = Thm.nprems_of goal;
val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks
- (Display_Goal.pretty_goals ctxt
+ (Goal_Display.pretty_goals ctxt
{total = true, main = ! show_main_goal, maxgoals = ! Display.goals_limit} goal @
[Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")])));
--- a/src/Pure/Proof/reconstruct.ML Sat Jul 25 00:53:47 2009 +0200
+++ b/src/Pure/Proof/reconstruct.ML Sat Jul 25 10:31:27 2009 +0200
@@ -255,7 +255,7 @@
let
fun search env [] = error ("Unsolvable constraints:\n" ^
Pretty.string_of (Pretty.chunks (map (fn (_, p, _) =>
- Display_Goal.pretty_flexpair (Syntax.init_pretty_global thy) (pairself
+ Goal_Display.pretty_flexpair (Syntax.init_pretty_global thy) (pairself
(Envir.norm_term bigenv) p)) cs)))
| search env ((u, p as (t1, t2), vs)::ps) =
if u then
--- a/src/Pure/ROOT.ML Sat Jul 25 00:53:47 2009 +0200
+++ b/src/Pure/ROOT.ML Sat Jul 25 10:31:27 2009 +0200
@@ -119,7 +119,7 @@
use "morphism.ML";
use "variable.ML";
use "conv.ML";
-use "display_goal.ML";
+use "goal_display.ML";
use "tactical.ML";
use "search.ML";
use "tactic.ML";
--- a/src/Pure/display.ML Sat Jul 25 00:53:47 2009 +0200
+++ b/src/Pure/display.ML Sat Jul 25 10:31:27 2009 +0200
@@ -42,8 +42,8 @@
(** options **)
-val goals_limit = Display_Goal.goals_limit;
-val show_consts = Display_Goal.show_consts;
+val goals_limit = Goal_Display.goals_limit;
+val show_consts = Goal_Display.show_consts;
val show_hyps = ref false; (*false: print meta-hypotheses as dots*)
val show_tags = ref false; (*false: suppress tags*)
@@ -87,7 +87,7 @@
if hlen = 0 andalso status = "" then []
else if ! show_hyps orelse show_hyps' then
[Pretty.brk 2, Pretty.list "[" "]"
- (map (q o Display_Goal.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @
+ (map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @
map (Syntax.pretty_sort ctxt) xshyps @
(if status = "" then [] else [Pretty.str status]))]
else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")];
--- a/src/Pure/display_goal.ML Sat Jul 25 00:53:47 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,124 +0,0 @@
-(* Title: Pure/display_goal.ML
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Author: Makarius
-
-Display tactical goal state.
-*)
-
-signature DISPLAY_GOAL =
-sig
- val goals_limit: int ref
- val show_consts: bool ref
- 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
-end;
-
-structure Display_Goal: DISPLAY_GOAL =
-struct
-
-val goals_limit = ref 10; (*max number of goals to print*)
-val show_consts = ref false; (*true: show consts with types in proof state output*)
-
-fun pretty_flexpair ctxt (t, u) = Pretty.block
- [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
-
-
-(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
-
-local
-
-fun ins_entry (x, y) =
- AList.default (op =) (x, []) #>
- AList.map_entry (op =) x (insert (op =) y);
-
-val add_consts = Term.fold_aterms
- (fn Const (c, T) => ins_entry (T, (c, T))
- | _ => I);
-
-val add_vars = Term.fold_aterms
- (fn Free (x, T) => ins_entry (T, (x, ~1))
- | Var (xi, T) => ins_entry (T, xi)
- | _ => I);
-
-val add_varsT = Term.fold_atyps
- (fn TFree (x, S) => ins_entry (S, (x, ~1))
- | TVar (xi, S) => ins_entry (S, xi)
- | _ => I);
-
-fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
-fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
-
-fun consts_of t = sort_cnsts (add_consts t []);
-fun vars_of t = sort_idxs (add_vars t []);
-fun varsT_of t = rev (sort_idxs (Term.fold_types add_varsT t []));
-
-in
-
-fun pretty_goals ctxt {total, main, maxgoals} state =
- let
- val prt_sort = Syntax.pretty_sort ctxt;
- val prt_typ = Syntax.pretty_typ ctxt;
- val prt_term = Syntax.pretty_term ctxt;
-
- fun prt_atoms prt prtT (X, xs) = Pretty.block
- [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
- Pretty.brk 1, prtT X];
-
- fun prt_var (x, ~1) = prt_term (Syntax.free x)
- | prt_var xi = prt_term (Syntax.var xi);
-
- fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
- | prt_varT xi = prt_typ (TVar (xi, []));
-
- val prt_consts = prt_atoms (prt_term o Const) prt_typ;
- val prt_vars = prt_atoms prt_var prt_typ;
- val prt_varsT = prt_atoms prt_varT prt_sort;
-
-
- fun pretty_list _ _ [] = []
- | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
-
- fun pretty_subgoal (n, A) = Pretty.markup Markup.subgoal
- [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A];
- fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
-
- val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt);
-
- val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
- val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
- val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
-
-
- val {prop, tpairs, ...} = Thm.rep_thm state;
- val (As, B) = Logic.strip_horn prop;
- val ngoals = length As;
-
- fun pretty_gs (types, sorts) =
- (if main then [prt_term B] else []) @
- (if ngoals = 0 then [Pretty.str "No subgoals!"]
- else if ngoals > maxgoals then
- pretty_subgoals (Library.take (maxgoals, As)) @
- (if total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
- else [])
- else pretty_subgoals As) @
- pretty_ffpairs tpairs @
- (if ! show_consts then pretty_consts prop else []) @
- (if types then pretty_vars prop else []) @
- (if sorts then pretty_varsT prop else []);
- in
- setmp show_no_free_types true
- (setmp show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
- (setmp show_sorts false pretty_gs))
- (! 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;
-
-end;
-
-end;
-
--- a/src/Pure/goal.ML Sat Jul 25 00:53:47 2009 +0200
+++ b/src/Pure/goal.ML Sat Jul 25 10:31:27 2009 +0200
@@ -78,7 +78,7 @@
(case Thm.nprems_of th of
0 => conclude th
| n => raise THM ("Proof failed.\n" ^
- Pretty.string_of (Pretty.chunks (Display_Goal.pretty_goals_without_context n th)) ^
+ Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals_without_context n th)) ^
("\n" ^ string_of_int n ^ " unsolved goal(s)!"), 0, [th]));
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/goal_display.ML Sat Jul 25 10:31:27 2009 +0200
@@ -0,0 +1,124 @@
+(* Title: Pure/goal_display.ML
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Makarius
+
+Display tactical goal state.
+*)
+
+signature GOAL_DISPLAY =
+sig
+ val goals_limit: int ref
+ val show_consts: bool ref
+ 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
+end;
+
+structure Goal_Display: GOAL_DISPLAY =
+struct
+
+val goals_limit = ref 10; (*max number of goals to print*)
+val show_consts = ref false; (*true: show consts with types in proof state output*)
+
+fun pretty_flexpair ctxt (t, u) = Pretty.block
+ [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
+
+
+(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
+
+local
+
+fun ins_entry (x, y) =
+ AList.default (op =) (x, []) #>
+ AList.map_entry (op =) x (insert (op =) y);
+
+val add_consts = Term.fold_aterms
+ (fn Const (c, T) => ins_entry (T, (c, T))
+ | _ => I);
+
+val add_vars = Term.fold_aterms
+ (fn Free (x, T) => ins_entry (T, (x, ~1))
+ | Var (xi, T) => ins_entry (T, xi)
+ | _ => I);
+
+val add_varsT = Term.fold_atyps
+ (fn TFree (x, S) => ins_entry (S, (x, ~1))
+ | TVar (xi, S) => ins_entry (S, xi)
+ | _ => I);
+
+fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
+fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
+
+fun consts_of t = sort_cnsts (add_consts t []);
+fun vars_of t = sort_idxs (add_vars t []);
+fun varsT_of t = rev (sort_idxs (Term.fold_types add_varsT t []));
+
+in
+
+fun pretty_goals ctxt {total, main, maxgoals} state =
+ let
+ val prt_sort = Syntax.pretty_sort ctxt;
+ val prt_typ = Syntax.pretty_typ ctxt;
+ val prt_term = Syntax.pretty_term ctxt;
+
+ fun prt_atoms prt prtT (X, xs) = Pretty.block
+ [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
+ Pretty.brk 1, prtT X];
+
+ fun prt_var (x, ~1) = prt_term (Syntax.free x)
+ | prt_var xi = prt_term (Syntax.var xi);
+
+ fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
+ | prt_varT xi = prt_typ (TVar (xi, []));
+
+ val prt_consts = prt_atoms (prt_term o Const) prt_typ;
+ val prt_vars = prt_atoms prt_var prt_typ;
+ val prt_varsT = prt_atoms prt_varT prt_sort;
+
+
+ fun pretty_list _ _ [] = []
+ | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
+
+ fun pretty_subgoal (n, A) = Pretty.markup Markup.subgoal
+ [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A];
+ fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
+
+ val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt);
+
+ val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
+ val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
+ val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
+
+
+ val {prop, tpairs, ...} = Thm.rep_thm state;
+ val (As, B) = Logic.strip_horn prop;
+ val ngoals = length As;
+
+ fun pretty_gs (types, sorts) =
+ (if main then [prt_term B] else []) @
+ (if ngoals = 0 then [Pretty.str "No subgoals!"]
+ else if ngoals > maxgoals then
+ pretty_subgoals (Library.take (maxgoals, As)) @
+ (if total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
+ else [])
+ else pretty_subgoals As) @
+ pretty_ffpairs tpairs @
+ (if ! show_consts then pretty_consts prop else []) @
+ (if types then pretty_vars prop else []) @
+ (if sorts then pretty_varsT prop else []);
+ in
+ setmp show_no_free_types true
+ (setmp show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
+ (setmp show_sorts false pretty_gs))
+ (! 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;
+
+end;
+
+end;
+
--- a/src/Pure/old_goals.ML Sat Jul 25 00:53:47 2009 +0200
+++ b/src/Pure/old_goals.ML Sat Jul 25 10:31:27 2009 +0200
@@ -125,7 +125,7 @@
special applications.*)
fun result_error_default state msg : thm =
Pretty.str "Bad final proof state:" ::
- Display_Goal.pretty_goals_without_context (!goals_limit) state @
+ Goal_Display.pretty_goals_without_context (!goals_limit) state @
[Pretty.str msg, Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error;
val result_error_fn = ref result_error_default;
@@ -267,7 +267,7 @@
(if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^
(if ngoals <> 1 then "s" else "") ^ ")"
else ""))] @
- Display_Goal.pretty_goals_without_context m th
+ Goal_Display.pretty_goals_without_context m th
end |> Pretty.chunks |> Pretty.writeln;
(*Printing can raise exceptions, so the assignment occurs last.
--- a/src/Pure/tactical.ML Sat Jul 25 00:53:47 2009 +0200
+++ b/src/Pure/tactical.ML Sat Jul 25 10:31:27 2009 +0200
@@ -194,7 +194,7 @@
fun print_tac msg st =
(tracing (msg ^ "\n" ^
Pretty.string_of (Pretty.chunks
- (Display_Goal.pretty_goals_without_context (! Display_Goal.goals_limit) st)));
+ (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st)));
Seq.single st);
(*Pause until a line is typed -- if non-empty then fail. *)
@@ -233,7 +233,7 @@
fun tracify flag tac st =
if !flag andalso not (!suppress_tracing) then
(tracing (Pretty.string_of (Pretty.chunks
- (Display_Goal.pretty_goals_without_context (! Display_Goal.goals_limit) st @
+ (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st @
[Pretty.str "** Press RETURN to continue:"])));
exec_trace_command flag (tac, st))
else tac st;