# HG changeset patch
# User wenzelm
# Date 1396262139 -7200
# Node ID 6b3739fee456ed44af90988445bfbbf4649d4a04
# Parent  38f1422ef473d97b7a2864d57844985bbd7bd7a8
some shortcuts for chunks, which sometimes avoid bulky string output;

diff -r 38f1422ef473 -r 6b3739fee456 src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Mon Mar 31 10:28:08 2014 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Mon Mar 31 12:35:39 2014 +0200
@@ -106,7 +106,7 @@
          Pretty.big_list (name ^ " " ^ f status)
            (Element.pretty_ctxt ctxt context' @
             Element.pretty_stmt ctxt stmt)) vcs'') vcs')] |>
-    Pretty.chunks2 |> Pretty.writeln
+    Pretty.writeln_chunks2
   end;
 
 val _ =
diff -r 38f1422ef473 -r 6b3739fee456 src/HOL/Tools/Quickcheck/find_unused_assms.ML
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Mon Mar 31 10:28:08 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Mon Mar 31 12:35:39 2014 +0200
@@ -106,7 +106,7 @@
     [Pretty.str (msg ^ ":"), Pretty.str ""] @
     map pretty_thm with_superfluous_assumptions @
     [Pretty.str "", Pretty.str end_msg]
-  end |> Pretty.chunks |> Pretty.writeln
+  end |> Pretty.writeln_chunks
 
 end
 
diff -r 38f1422ef473 -r 6b3739fee456 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Mon Mar 31 10:28:08 2014 +0200
+++ b/src/HOL/Tools/inductive.ML	Mon Mar 31 12:35:39 2014 +0200
@@ -232,7 +232,7 @@
         (Pretty.str "(co)inductives:" ::
           map (Pretty.mark_str o #1) (Name_Space.markup_entries ctxt space (Symtab.dest infos)))),
      Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_item ctxt) monos)]
-  end |> Pretty.chunks |> Pretty.writeln;
+  end |> Pretty.writeln_chunks;
 
 
 (* inductive info *)
diff -r 38f1422ef473 -r 6b3739fee456 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Mon Mar 31 10:28:08 2014 +0200
+++ b/src/Provers/classical.ML	Mon Mar 31 12:35:39 2014 +0200
@@ -632,7 +632,7 @@
       Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs),
       Pretty.strs ("safe wrappers:" :: map #1 swrappers),
       Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)]
-    |> Pretty.chunks |> Pretty.writeln
+    |> Pretty.writeln_chunks
   end;
 
 
diff -r 38f1422ef473 -r 6b3739fee456 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Mon Mar 31 10:28:08 2014 +0200
+++ b/src/Pure/General/output.ML	Mon Mar 31 12:35:39 2014 +0200
@@ -25,6 +25,7 @@
   val physical_stderr: output -> unit
   val physical_writeln: output -> unit
   exception Protocol_Message of Properties.T
+  val writelns: string list -> unit
   val urgent_message: string -> unit
   val error_message': serial * string -> unit
   val error_message: string -> unit
@@ -107,7 +108,8 @@
 val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref =
   Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props);
 
-fun writeln s = ! writeln_fn [output s];
+fun writelns ss = ! writeln_fn (map output ss);
+fun writeln s = writelns [s];
 fun urgent_message s = ! urgent_message_fn [output s];  (*Proof General legacy*)
 fun tracing s = ! tracing_fn [output s];
 fun warning s = ! warning_fn [output s];
diff -r 38f1422ef473 -r 6b3739fee456 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Mon Mar 31 10:28:08 2014 +0200
+++ b/src/Pure/General/pretty.ML	Mon Mar 31 12:35:39 2014 +0200
@@ -45,10 +45,6 @@
   val text: string -> T list
   val paragraph: T list -> T
   val para: string -> T
-  val markup_chunks: Markup.T -> T list -> T
-  val chunks: T list -> T
-  val chunks2: T list -> T
-  val block_enclose: T * T -> T list -> T
   val quote: T -> T
   val backquote: T -> T
   val cartouche: T -> T
@@ -72,6 +68,12 @@
   val symbolic_output: T -> Output.output
   val symbolic_string_of: T -> string
   val str_of: T -> string
+  val markup_chunks: Markup.T -> T list -> T
+  val chunks: T list -> T
+  val chunks2: T list -> T
+  val block_enclose: T * T -> T list -> T
+  val writeln_chunks: T list -> unit
+  val writeln_chunks2: T list -> unit
   val to_ML: T -> ML_Pretty.pretty
   val from_ML: ML_Pretty.pretty -> T
 end;
@@ -170,17 +172,6 @@
 val paragraph = markup Markup.paragraph;
 val para = paragraph o text;
 
-fun markup_chunks m prts = markup m (fbreaks (map (text_fold o single) prts));
-val chunks = markup_chunks Markup.empty;
-
-fun chunks2 prts =
-  (case try split_last prts of
-    NONE => blk (0, [])
-  | SOME (prefix, last) =>
-      blk (0, maps (fn prt => [text_fold [prt, fbrk], fbrk]) prefix @ [text_fold [last]]));
-
-fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2];
-
 fun quote prt = blk (1, [str "\"", prt, str "\""]);
 fun backquote prt = blk (1, [str "`", prt, str "`"]);
 fun cartouche prt = blk (1, [str "\\<open>", prt, str "\\<close>"]);
@@ -355,6 +346,33 @@
 val str_of = Output.escape o Buffer.content o unformatted;
 
 
+(* chunks *)
+
+fun markup_chunks m prts = markup m (fbreaks (map (text_fold o single) prts));
+val chunks = markup_chunks Markup.empty;
+
+fun chunks2 prts =
+  (case try split_last prts of
+    NONE => blk (0, [])
+  | SOME (prefix, last) =>
+      blk (0, maps (fn prt => [text_fold [prt, fbrk], fbrk]) prefix @ [text_fold [last]]));
+
+fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2];
+
+fun string_of_text_fold prt = string_of prt |> Markup.markup Markup.text_fold;
+
+fun writeln_chunks prts =
+  Output.writelns (Library.separate "\n" (map string_of_text_fold prts));
+
+fun writeln_chunks2 prts =
+  (case try split_last prts of
+    NONE => ()
+  | SOME (prefix, last) =>
+      (map (fn prt => Markup.markup Markup.text_fold (string_of prt ^ "\n") ^ "\n") prefix @
+        [string_of_text_fold last])
+      |> Output.writelns);
+
+
 
 (** ML toplevel pretty printing **)
 
diff -r 38f1422ef473 -r 6b3739fee456 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Mar 31 10:28:08 2014 +0200
+++ b/src/Pure/Isar/attrib.ML	Mon Mar 31 12:35:39 2014 +0200
@@ -105,7 +105,7 @@
             (Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
   in
     [Pretty.big_list "attributes:" (map prt_attr (Name_Space.markup_table ctxt attribs))]
-    |> Pretty.chunks |> Pretty.writeln
+    |> Pretty.writeln_chunks
   end;
 
 val attribute_space = Name_Space.space_of_table o get_attributes o Context.Proof;
diff -r 38f1422ef473 -r 6b3739fee456 src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Mon Mar 31 10:28:08 2014 +0200
+++ b/src/Pure/Isar/bundle.ML	Mon Mar 31 12:35:39 2014 +0200
@@ -134,7 +134,7 @@
         Pretty.breaks (Pretty.str " =" :: maps prt_fact bundle));
   in
     map prt_bundle (Name_Space.markup_table ctxt (get_bundles ctxt))
-  end |> Pretty.chunks |> Pretty.writeln;
+  end |> Pretty.writeln_chunks;
 
 end;
 
diff -r 38f1422ef473 -r 6b3739fee456 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Mon Mar 31 10:28:08 2014 +0200
+++ b/src/Pure/Isar/calculation.ML	Mon Mar 31 12:35:39 2014 +0200
@@ -46,7 +46,7 @@
   in
    [Pretty.big_list "transitivity rules:" (map pretty_thm (Item_Net.content trans)),
     Pretty.big_list "symmetry rules:" (map pretty_thm sym)]
-  end |> Pretty.chunks |> Pretty.writeln;
+  end |> Pretty.writeln_chunks;
 
 
 (* access calculation *)
diff -r 38f1422ef473 -r 6b3739fee456 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Mon Mar 31 10:28:08 2014 +0200
+++ b/src/Pure/Isar/class.ML	Mon Mar 31 12:35:39 2014 +0200
@@ -203,8 +203,7 @@
     Sorts.all_classes algebra
     |> sort (Name_Space.extern_ord ctxt class_space)
     |> map prt_entry
-    |> Pretty.chunks2
-    |> Pretty.writeln
+    |> Pretty.writeln_chunks2
   end;
 
 
diff -r 38f1422ef473 -r 6b3739fee456 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon Mar 31 10:28:08 2014 +0200
+++ b/src/Pure/Isar/code.ML	Mon Mar 31 12:35:39 2014 +0200
@@ -1036,7 +1036,7 @@
     val cases = Symtab.dest ((fst o the_cases o the_exec) thy);
     val undefineds = Symtab.keys ((snd o the_cases o the_exec) thy);
   in
-    (Pretty.writeln o Pretty.chunks) [
+    Pretty.writeln_chunks [
       Pretty.block (
         Pretty.str "code equations:" :: Pretty.fbrk
         :: (Pretty.fbreaks o map pretty_function) functions
diff -r 38f1422ef473 -r 6b3739fee456 src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Mon Mar 31 10:28:08 2014 +0200
+++ b/src/Pure/Isar/context_rules.ML	Mon Mar 31 12:35:39 2014 +0200
@@ -120,7 +120,7 @@
         (map_filter (fn (_, (k, th)) =>
             if k = (i, b) then SOME (Display.pretty_thm_item ctxt th) else NONE)
           (sort (int_ord o pairself fst) rules));
-  in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
+  in Pretty.writeln_chunks (map prt_kind rule_kinds) end;
 
 
 (* access data *)
diff -r 38f1422ef473 -r 6b3739fee456 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Mon Mar 31 10:28:08 2014 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Mon Mar 31 12:35:39 2014 +0200
@@ -333,7 +333,7 @@
         NONE => (Theory.parents_of thy, [thy])
       | SOME (xs, NONE) => (map get_theory xs, [thy])
       | SOME (xs, SOME ys) => (map get_theory xs, map get_theory ys))
-    |> map pretty_thm |> Pretty.chunks |> Pretty.writeln
+    |> map pretty_thm |> Pretty.writeln_chunks
   end);
 
 
diff -r 38f1422ef473 -r 6b3739fee456 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Mon Mar 31 10:28:08 2014 +0200
+++ b/src/Pure/Isar/method.ML	Mon Mar 31 12:35:39 2014 +0200
@@ -328,7 +328,7 @@
             (Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
   in
     [Pretty.big_list "methods:" (map prt_meth (Name_Space.markup_table ctxt meths))]
-    |> Pretty.chunks |> Pretty.writeln
+    |> Pretty.writeln_chunks
   end;
 
 fun add_method name meth comment thy = thy
diff -r 38f1422ef473 -r 6b3739fee456 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Mar 31 10:28:08 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Mar 31 12:35:39 2014 +0200
@@ -219,7 +219,7 @@
   dest_commands (#2 (get_syntax ()))
   |> filter (fn (name, _) => forall (fn pat => match_string pat name) pats)
   |> map pretty_command
-  |> Pretty.chunks |> Pretty.writeln;
+  |> Pretty.writeln_chunks;
 
 fun print_outer_syntax () =
   let
@@ -231,7 +231,7 @@
     [Pretty.strs ("syntax keywords:" :: map quote keywords),
       Pretty.big_list "commands:" (map pretty_command cmds),
       Pretty.big_list "interactive-only commands:" (map pretty_command int_cmds)]
-    |> Pretty.chunks |> Pretty.writeln
+    |> Pretty.writeln_chunks
   end;
 
 
diff -r 38f1422ef473 -r 6b3739fee456 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Mar 31 10:28:08 2014 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Mar 31 12:35:39 2014 +0200
@@ -1250,7 +1250,7 @@
     else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)]
   end;
 
-val print_abbrevs = Pretty.writeln o Pretty.chunks o pretty_abbrevs true;
+val print_abbrevs = Pretty.writeln_chunks o pretty_abbrevs true;
 
 
 (* term bindings *)
@@ -1264,7 +1264,7 @@
     else [Pretty.big_list "term bindings:" (map prt_bind (Vartab.dest binds))]
   end;
 
-val print_binds = Pretty.writeln o Pretty.chunks o pretty_binds;
+val print_binds = Pretty.writeln_chunks o pretty_binds;
 
 
 (* local facts *)
@@ -1284,7 +1284,7 @@
   end;
 
 fun print_local_facts ctxt verbose =
-  Pretty.writeln (Pretty.chunks (pretty_local_facts ctxt verbose));
+  Pretty.writeln_chunks (pretty_local_facts ctxt verbose);
 
 
 (* local contexts *)
@@ -1331,7 +1331,7 @@
     else [Pretty.big_list "cases:" (map pretty_case cases)]
   end;
 
-val print_cases = Pretty.writeln o Pretty.chunks o pretty_cases;
+val print_cases = Pretty.writeln_chunks o pretty_cases;
 
 end;
 
diff -r 38f1422ef473 -r 6b3739fee456 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Mar 31 10:28:08 2014 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon Mar 31 12:35:39 2014 +0200
@@ -205,7 +205,7 @@
   | SOME (Theory (gthy, _)) => pretty_context gthy
   | SOME (Proof (_, (_, gthy))) => pretty_context gthy
   | SOME (Skipped_Proof (_, (gthy, _))) => pretty_context gthy)
-  |> Pretty.chunks |> Pretty.writeln;
+  |> Pretty.writeln_chunks;
 
 fun print_state prf_only state =
   (case try node_of state of
diff -r 38f1422ef473 -r 6b3739fee456 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon Mar 31 10:28:08 2014 +0200
+++ b/src/Pure/Syntax/syntax.ML	Mon Mar 31 12:35:39 2014 +0200
@@ -575,9 +575,9 @@
 
 in
 
-fun print_gram syn = Pretty.writeln (Pretty.chunks (pretty_gram syn));
-fun print_trans syn = Pretty.writeln (Pretty.chunks (pretty_trans syn));
-fun print_syntax syn = Pretty.writeln (Pretty.chunks (pretty_gram syn @ pretty_trans syn));
+fun print_gram syn = Pretty.writeln_chunks (pretty_gram syn);
+fun print_trans syn = Pretty.writeln_chunks (pretty_trans syn);
+fun print_syntax syn = Pretty.writeln_chunks (pretty_gram syn @ pretty_trans syn);
 
 end;
 
diff -r 38f1422ef473 -r 6b3739fee456 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Mon Mar 31 10:28:08 2014 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Mon Mar 31 12:35:39 2014 +0200
@@ -878,7 +878,7 @@
     pretty_checks "term_checks" term_checks @
     pretty_checks "typ_unchecks" typ_unchecks @
     pretty_checks "term_unchecks" term_unchecks
-  end |> Pretty.chunks |> Pretty.writeln;
+  end |> Pretty.writeln_chunks;
 
 
 local
diff -r 38f1422ef473 -r 6b3739fee456 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Mar 31 10:28:08 2014 +0200
+++ b/src/Pure/Thy/thy_output.ML	Mon Mar 31 12:35:39 2014 +0200
@@ -109,7 +109,7 @@
   in
     [Pretty.big_list "document antiquotations:" (map Pretty.mark_str command_names),
       Pretty.big_list "document antiquotation options:" (map Pretty.mark_str option_names)]
-    |> Pretty.chunks |> Pretty.writeln
+    |> Pretty.writeln_chunks
   end;
 
 fun antiquotation name scan body =
diff -r 38f1422ef473 -r 6b3739fee456 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Mon Mar 31 10:28:08 2014 +0200
+++ b/src/Tools/Code/code_preproc.ML	Mon Mar 31 12:35:39 2014 +0200
@@ -181,7 +181,7 @@
     val post = (#post o the_thmproc) thy;
     val functrans = (map fst o #functrans o the_thmproc) thy;
   in
-    (Pretty.writeln o Pretty.chunks) [
+    Pretty.writeln_chunks [
       Pretty.block [
         Pretty.str "preprocessing simpset:",
         Pretty.fbrk,
diff -r 38f1422ef473 -r 6b3739fee456 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Mon Mar 31 10:28:08 2014 +0200
+++ b/src/Tools/induct.ML	Mon Mar 31 12:35:39 2014 +0200
@@ -254,7 +254,7 @@
     pretty_rules ctxt "induct pred:" inductP,
     pretty_rules ctxt "cases type:" casesT,
     pretty_rules ctxt "cases pred:" casesP]
-    |> Pretty.chunks |> Pretty.writeln
+    |> Pretty.writeln_chunks
   end;
 
 val _ =
diff -r 38f1422ef473 -r 6b3739fee456 src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Mon Mar 31 10:28:08 2014 +0200
+++ b/src/Tools/subtyping.ML	Mon Mar 31 12:35:39 2014 +0200
@@ -1085,7 +1085,7 @@
    [Pretty.big_list "coercions between base types:" (map show_coercion simple),
     Pretty.big_list "other coercions:" (map show_coercion complex),
     Pretty.big_list "coercion maps:" (map show_map tmaps)]
-  end |> Pretty.chunks |> Pretty.writeln;
+  end |> Pretty.writeln_chunks;
 
 
 (* theory setup *)