# HG changeset patch # User wenzelm # Date 953141213 -3600 # Node ID 7f4e4e875c13edb5ba29fb4539f9b26d1f27597f # Parent 2693a3a9fcc147bf1dc2aaaedd43196cbb178ca6 pretty chunks; diff -r 2693a3a9fcc1 -r 7f4e4e875c13 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Wed Mar 15 18:25:42 2000 +0100 +++ b/src/Pure/Isar/proof.ML Wed Mar 15 18:26:53 2000 +0100 @@ -304,9 +304,9 @@ val verbose = ProofContext.verbose; -fun print_facts _ None = () - | print_facts s (Some ths) = - (Pretty.writeln (Pretty.big_list (s ^ "this:") (map pretty_thm ths)); writeln ""); +fun pretty_facts _ None = [] + | pretty_facts s (Some ths) = + [Pretty.big_list (s ^ "this:") (map pretty_thm ths), Pretty.str ""]; fun print_state nr (state as State (Node {context, facts, mode, goal = _}, nodes)) = let @@ -316,27 +316,27 @@ | levels_up 1 = ", 1 level up" | levels_up i = ", " ^ string_of_int i ^ " levels up"; - fun print_goal (_, (i, (((kind, name, _), (goal_facts, thm)), _))) = - (print_facts "using " - (if mode <> Backward orelse null goal_facts then None else Some goal_facts); - writeln ("goal (" ^ kind_name kind ^ (if name = "" then "" else " " ^ name) ^ - levels_up (i div 2) ^ "):"); - Locale.print_goals_marker begin_goal (! goals_limit) thm); + fun pretty_goal (_, (i, (((kind, name, _), (goal_facts, thm)), _))) = + pretty_facts "using " + (if mode <> Backward orelse null goal_facts then None else Some goal_facts) @ + [Pretty.str ("goal (" ^ kind_name kind ^ (if name = "" then "" else " " ^ name) ^ + levels_up (i div 2) ^ "):")] @ + Locale.pretty_goals_marker begin_goal (! goals_limit) thm; - val ctxt_strings = - if ! verbose orelse mode = Forward then ProofContext.strings_of_context context - else if mode = Backward then ProofContext.strings_of_prems context + val ctxt_prts = + if ! verbose orelse mode = Forward then ProofContext.pretty_context context + else if mode = Backward then ProofContext.pretty_prems context else []; - in - writeln ("Proof(" ^ mode_name mode ^ "): step " ^ string_of_int nr ^ - ", depth " ^ string_of_int (length nodes div 2)); - writeln ""; - if null ctxt_strings then () else (seq writeln ctxt_strings; writeln ""); - if ! verbose orelse mode = Forward then - (print_facts "" facts; print_goal (find_goal 0 state)) - else if mode = ForwardChain then print_facts "picking " facts - else print_goal (find_goal 0 state) - end; + + val prts = + [Pretty.str ("Proof(" ^ mode_name mode ^ "): step " ^ string_of_int nr ^ + ", depth " ^ string_of_int (length nodes div 2)), Pretty.str ""] @ + (if null ctxt_prts then [] else ctxt_prts @ [Pretty.str ""]) @ + (if ! verbose orelse mode = Forward then + (pretty_facts "" facts @ pretty_goal (find_goal 0 state)) + else if mode = ForwardChain then pretty_facts "picking " facts + else pretty_goal (find_goal 0 state)) + in Pretty.writeln (Pretty.chunks prts) end; diff -r 2693a3a9fcc1 -r 7f4e4e875c13 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Wed Mar 15 18:25:42 2000 +0100 +++ b/src/Pure/Isar/proof_context.ML Wed Mar 15 18:26:53 2000 +0100 @@ -18,8 +18,8 @@ val print_binds: context -> unit val print_thms: context -> unit val print_cases: context -> unit - val strings_of_prems: context -> string list - val strings_of_context: context -> string list + val pretty_prems: context -> Pretty.T list + val pretty_context: context -> Pretty.T list val print_proof_data: theory -> unit val init: theory -> context val read_typ: context -> string -> typ @@ -136,15 +136,15 @@ val verbose = ref false; fun verb f x = if ! verbose then f (x ()) else []; -val verb_string = verb (Library.single o Pretty.string_of); +fun verb_single x = verb Library.single x; -fun strings_of_items prt name items = +fun pretty_items prt name items = let - fun pretty_itms (name, [x]) = Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt x] - | pretty_itms (name, xs) = Pretty.big_list (name ^ ":") (map prt xs); + fun prt_itms (name, [x]) = Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt x] + | prt_itms (name, xs) = Pretty.big_list (name ^ ":") (map prt xs); in if null items andalso not (! verbose) then [] - else [Pretty.string_of (Pretty.big_list name (map pretty_itms items))] + else [Pretty.big_list name (map prt_itms items)] end; @@ -152,30 +152,30 @@ val smash_option = fn (_, None) => None | (xi, Some b) => Some (xi, b); -fun strings_of_binds (ctxt as Context {binds, ...}) = +fun pretty_binds (ctxt as Context {binds, ...}) = let val prt_term = Sign.pretty_term (sign_of ctxt); - fun pretty_bind (xi, (t, T)) = prt_term (Logic.mk_equals (Var (xi, T), t)); + fun prt_bind (xi, (t, T)) = prt_term (Logic.mk_equals (Var (xi, T), t)); val bs = mapfilter smash_option (Vartab.dest binds); in if null bs andalso not (! verbose) then [] - else [Pretty.string_of (Pretty.big_list "term bindings:" (map pretty_bind bs))] + else [Pretty.big_list "term bindings:" (map prt_bind bs)] end; -val print_binds = seq writeln o strings_of_binds; +val print_binds = Pretty.writeln o Pretty.chunks o pretty_binds; (* local theorems *) -fun strings_of_thms (Context {thms, ...}) = - strings_of_items pretty_thm "local theorems:" (mapfilter smash_option (Symtab.dest thms)); +fun pretty_thms (Context {thms, ...}) = + pretty_items pretty_thm "local theorems:" (mapfilter smash_option (Symtab.dest thms)); -val print_thms = seq writeln o strings_of_thms; +val print_thms = Pretty.writeln o Pretty.chunks o pretty_thms; (* local contexts *) -fun strings_of_cases (ctxt as Context {cases, ...}) = +fun pretty_cases (ctxt as Context {cases, ...}) = let val prt_term = Sign.pretty_term (sign_of ctxt); @@ -190,20 +190,20 @@ val cases' = rev (Library.gen_distinct Library.eq_fst cases); in if null cases andalso not (! verbose) then [] - else [Pretty.string_of (Pretty.big_list "cases:" (map prt_case cases'))] + else [Pretty.big_list "cases:" (map prt_case cases')] end; -val print_cases = seq writeln o strings_of_cases; +val print_cases = Pretty.writeln o Pretty.chunks o pretty_cases; (* main context *) -fun strings_of_prems ctxt = +fun pretty_prems ctxt = (case prems_of ctxt of [] => [] - | prems => [Pretty.string_of (Pretty.big_list "prems:" (map pretty_thm prems))]); + | prems => [Pretty.big_list "prems:" (map pretty_thm prems)]); -fun strings_of_context (ctxt as Context {asms = (_, (fixes, _)), cases, +fun pretty_context (ctxt as Context {asms = (_, (fixes, _)), cases, defs = (types, sorts, used), ...}) = let val sign = sign_of ctxt; @@ -235,15 +235,15 @@ val prt_defT = prt_atom prt_var prt_typ; val prt_defS = prt_atom prt_varT prt_sort; in - verb_string (K pretty_thy) @ - (if null fixes then [] else [Pretty.string_of (prt_fixes (rev fixes))]) @ - strings_of_prems ctxt @ - verb strings_of_binds (K ctxt) @ - verb strings_of_thms (K ctxt) @ - verb strings_of_cases (K ctxt) @ - verb_string (fn () => Pretty.big_list "type constraints:" (map prt_defT (Vartab.dest types))) @ - verb_string (fn () => Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts))) @ - verb_string (fn () => Pretty.strs ("used type variable names:" :: used)) + verb_single (K pretty_thy) @ + (if null fixes then [] else [prt_fixes (rev fixes)]) @ + pretty_prems ctxt @ + verb pretty_binds (K ctxt) @ + verb pretty_thms (K ctxt) @ + verb pretty_cases (K ctxt) @ + verb_single (fn () => Pretty.big_list "type constraints:" (map prt_defT (Vartab.dest types))) @ + verb_single (fn () => Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts))) @ + verb_single (fn () => Pretty.strs ("used type variable names:" :: used)) end; @@ -366,7 +366,6 @@ handle TYPE (msg, _, _) => raise CONTEXT (msg, ctxt); - (* internalize Skolem constants *) fun get_skolem (Context {asms = (_, (fixes, _)), ...}) x = assoc (fixes, x);