--- a/src/HOL/Spec_Check/output_style.ML Thu May 30 22:26:16 2013 +0200
+++ b/src/HOL/Spec_Check/output_style.ML Thu May 30 22:30:38 2013 +0200
@@ -49,7 +49,7 @@
StringCvt.padRight #" " countw (ratio (#count stats, length badobjs))
fun status (_, result, (stats, badobjs)) =
- if Property.failure result then writeln (update (stats, badobjs) false) else ()
+ if Property.failure result then warning (update (stats, badobjs) false) else ()
fun prtag count (tag, n) first =
if String.isPrefix "__" tag then ("", first)
@@ -69,7 +69,7 @@
let
fun iter [] _ = ()
| iter (e :: es) k =
- (writeln (StringCvt.padLeft #" " namew (if k > 0 then "" else "counter-examples") ^
+ (warning (StringCvt.padLeft #" " namew (if k > 0 then "" else "counter-examples") ^
StringCvt.padRight #" " resultw (if k > 0 then "" else ":") ^ e);
iter es (k + 1))
in
@@ -78,7 +78,7 @@
fun finish (stats, badobjs) =
if null badobjs then writeln (update (stats, badobjs) true ^ prtags stats)
- else (writeln (update (stats, badobjs) true); err badobjs)
+ else (warning (update (stats, badobjs) true); err badobjs)
in
{status = status, finish = finish}
end)
@@ -95,7 +95,7 @@
val _ = writeln ("[testing " ^ tag ^ "... ")
fun finish ({count, ...}, badobjs) =
(case (count, badobjs) of
- (0, []) => writeln ("no valid cases generated]")
+ (0, []) => warning ("no valid cases generated]")
| (n, []) => writeln (
if n >= gen_target then "ok]"
else "ok on " ^ string_of_int n ^ "; " ^ string_of_int gen_target ^ " required]")
@@ -103,9 +103,9 @@
let
val wd = size (string_of_int (length es))
fun each (NONE, _) = ()
- | each (SOME e, i) = writeln (tag ^ ":" ^ pad wd i ^ ".0 Error: " ^ e)
+ | each (SOME e, i) = warning (tag ^ ":" ^ pad wd i ^ ".0 Error: " ^ e)
in
- (writeln "FAILED]"; map each (es ~~ (1 upto (length es))); ())
+ (warning "FAILED]"; map each (es ~~ (1 upto (length es))); ())
end)
in
{status = K (), finish = finish}