# 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}