# HG changeset patch
# User berghofe
# Date 1295194873 -3600
# Node ID 74c0629a11e9448188df096aaf39ee4d862feef2
# Parent  bbd861837ebc01b29283130e5605961f4beb7c54
Tuned show_status

diff -r bbd861837ebc -r 74c0629a11e9 src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Sun Jan 16 15:53:03 2011 +0100
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Sun Jan 16 17:21:13 2011 +0100
@@ -64,9 +64,6 @@
 fun string_of_status false = "(unproved)"
   | string_of_status true = "(proved)";
 
-fun chunks ps = Pretty.blk (0,
-  flat (separate [Pretty.fbrk, Pretty.fbrk] (map single ps)));
-
 fun show_status (p, f) = Toplevel.no_timing o Toplevel.keep (fn state =>
   let
     val thy = Toplevel.theory_of state;
@@ -84,27 +81,24 @@
       ProofContext.init_global |>
       Context.proof_map (fold Element.init context)
   in
-    (* FIXME print as single message, e.g. via Pretty.big_list, Pretty.chunks etc. *)
-    (writeln "Context:\n";
-     Pretty.chunks (maps (Element.pretty_ctxt ctxt) context) |>
-     Pretty.writeln;
+    [Pretty.str "Context:",
+     Pretty.chunks (maps (Element.pretty_ctxt ctxt) context),
 
-     writeln "\nDefinitions:\n";
+     Pretty.str "Definitions:",
      Pretty.chunks (map (fn (bdg, th) => Pretty.block
        [Pretty.str (Binding.str_of bdg ^ ":"),
         Pretty.brk 1,
         Display.pretty_thm ctxt th])
-          defs) |>
-     Pretty.writeln;
+          defs),
 
-     writeln "\nVerification conditions:\n";
-     chunks (maps (fn (trace, vcs'') =>
+     Pretty.str "Verification conditions:",
+     Pretty.chunks2 (maps (fn (trace, vcs'') =>
        Pretty.str trace ::
        map (fn (name, status, context', stmt) =>
          Pretty.big_list (name ^ " " ^ f status)
            (Element.pretty_ctxt ctxt context' @
-            Element.pretty_stmt ctxt stmt)) vcs'') vcs') |>
-     Pretty.writeln)
+            Element.pretty_stmt ctxt stmt)) vcs'') vcs')] |>
+    Pretty.chunks2 |> Pretty.writeln
   end);
 
 val _ =