--- a/src/HOL/Spec_Check/output_style.ML Thu May 30 20:20:23 2013 +0200
+++ b/src/HOL/Spec_Check/output_style.ML Thu May 30 20:26:27 2013 +0200
@@ -40,7 +40,7 @@
^ (padRight #" " countw (ratio (#count stats, length badobjs)))
fun status (_, result, (stats, badobjs)) =
- if Property.failure result then Output.writeln (update (stats, badobjs) false) else ()
+ if Property.failure result then writeln (update (stats, badobjs) false) else ()
fun prtag count (tag, n) first =
if String.isPrefix "__" tag then ("", first)
@@ -60,7 +60,7 @@
let
fun iter [] _ = ()
| iter (e :: es) k =
- (Output.writeln (padLeft #" " namew (if k > 0 then "" else "counter-examples")
+ (writeln (padLeft #" " namew (if k > 0 then "" else "counter-examples")
^ padRight #" " resultw (if k > 0 then "" else ":") ^ e);
iter es (k + 1))
in
@@ -68,8 +68,8 @@
end
fun finish (stats, badobjs) =
- if null badobjs then Output.writeln (update (stats, badobjs) true ^ prtags stats)
- else (Output.writeln (update (stats, badobjs) true); err badobjs)
+ if null badobjs then writeln (update (stats, badobjs) true ^ prtags stats)
+ else (writeln (update (stats, badobjs) true); err badobjs)
in
{status=status, finish=finish}
end
@@ -92,19 +92,19 @@
fun new ctxt tag =
let
val gen_target = Config.get_generic ctxt Spec_Check.gen_target
- val _ = Output.writeln ("[testing " ^ tag ^ "... ") (* TODO: Output without line break *)
+ val _ = writeln ("[testing " ^ tag ^ "... ") (* TODO: Output without line break *)
fun finish ({count, ...}, badobjs) = case (count, badobjs) of
- (0, []) => Output.writeln ("no valid cases generated]")
- | (n, []) => Output.writeln (
+ (0, []) => writeln ("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]")
| (_, es) =>
let
val wd = size (string_of_int (length es))
fun each (NONE, _) = ()
- | each (SOME e, i) = Output.writeln (tag ^ ":" ^ pad wd i ^ ".0 Error: " ^ e)
+ | each (SOME e, i) = writeln (tag ^ ":" ^ pad wd i ^ ".0 Error: " ^ e)
in
- (Output.writeln "FAILED]"; map each (es ~~ (1 upto (length es))); ())
+ (writeln "FAILED]"; map each (es ~~ (1 upto (length es))); ())
end
in
{status = K (), finish = finish}