pretty chunks;

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

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