# 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 _ =