# HG changeset patch
# User wenzelm
# Date 1374097870 -7200
# Node ID b24d11ab44ff1095dfadaae0ceac66f346af6861
# Parent  9306c309b892cb7a68190618e074b399ba73878f# Parent  da646aa4a3bbd21e7fa52b20ad84f9bde8501a53
merged

diff -r 9306c309b892 -r b24d11ab44ff src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Wed Jul 17 23:36:33 2013 +0200
+++ b/src/Pure/General/pretty.ML	Wed Jul 17 23:51:10 2013 +0200
@@ -39,6 +39,7 @@
   val mark_str: Markup.T * string -> T
   val marks_str: Markup.T list * string -> T
   val item: T list -> T
+  val text_fold: T list -> T
   val command: string -> T
   val keyword: string -> T
   val text: string -> T list
@@ -159,6 +160,7 @@
 fun marks_str (ms, s) = fold_rev mark ms (str s);
 
 val item = markup Markup.item;
+val text_fold = markup Markup.text_fold;
 
 fun command name = mark_str (Markup.keyword1, name);
 fun keyword name = mark_str (Markup.keyword2, name);
@@ -167,16 +169,14 @@
 val paragraph = markup Markup.paragraph;
 val para = paragraph o text;
 
-fun markup_chunks m prts = markup m (fbreaks (map (mark Markup.text_fold) prts));
+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 => [markup Markup.text_fold [prt, fbrk], fbrk]) prefix @
-        [mark Markup.text_fold 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];
 
diff -r 9306c309b892 -r b24d11ab44ff src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Wed Jul 17 23:36:33 2013 +0200
+++ b/src/Tools/quickcheck.ML	Wed Jul 17 23:51:10 2013 +0200
@@ -398,17 +398,20 @@
 fun pretty_counterex ctxt auto NONE =
     Pretty.str (tool_name auto ^ " found no counterexample." ^ Config.get ctxt tag)
   | pretty_counterex ctxt auto (SOME ((genuine, cex), eval_terms)) =
-      Pretty.chunks ((Pretty.str (tool_name auto ^ " found a " ^
-        (if genuine then "counterexample:"
-          else "potentially spurious counterexample due to underspecified functions:")
-          ^ Config.get ctxt tag ^ "\n") ::
-        map (fn (s, t) =>
-          Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) (rev cex))
-        @ (if null eval_terms then []
-           else (Pretty.fbrk :: Pretty.str ("Evaluated terms:") ::
-             map (fn (t, u) =>
-               Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1,
-                 Syntax.pretty_term ctxt u]) (rev eval_terms))));
+      (Pretty.text_fold o Pretty.fbreaks)
+        (Pretty.str (tool_name auto ^ " found a " ^
+         (if genuine then "counterexample:"
+          else "potentially spurious counterexample due to underspecified functions:") ^
+         Config.get ctxt tag) ::
+         Pretty.str "" ::
+         map (fn (s, t) =>
+          Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) (rev cex) @
+         (if null eval_terms then []
+          else
+           Pretty.str "" :: Pretty.str "Evaluated terms:" ::
+           map (fn (t, u) =>
+            Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1,
+             Syntax.pretty_term ctxt u]) (rev eval_terms)));
 
 
 (* Isar commands *)