# HG changeset patch
# User wenzelm
# Date 1222277965 -7200
# Node ID 4562584d9d66a69e6835e2a9ecdbeec13a2991f7
# Parent  f4a17868bde576a025623e8fcfbac4d0059433f9
report: produce individual status messages;

diff -r f4a17868bde5 -r 4562584d9d66 src/Pure/Isar/outer_keyword.ML
--- a/src/Pure/Isar/outer_keyword.ML	Wed Sep 24 19:33:14 2008 +0200
+++ b/src/Pure/Isar/outer_keyword.ML	Wed Sep 24 19:39:25 2008 +0200
@@ -148,7 +148,7 @@
   let val (keywords, commands) = CRITICAL (fn () =>
     (dest_keywords (), sort_wrt #1 (Symtab.dest (get_commands ()))))
   in map report_keyword keywords @ map report_command commands end
-  |> Pretty.chunks |> Pretty.string_of |> Output.status;
+  |> List.app (Output.status o Pretty.string_of);
 
 
 (* augment tables *)