# HG changeset patch # User wenzelm # Date 1369945838 -7200 # Node ID cdba0c3cb4c264e39dee1cbfe8f5f2a820ff2708 # Parent 320c86e50f84820f4c5d72d32a479ec6a4499a8f tuned messages -- some attempts to observe Isabelle output channel semantics; diff -r 320c86e50f84 -r cdba0c3cb4c2 src/HOL/Spec_Check/output_style.ML --- 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}