# HG changeset patch
# User wenzelm
# Date 1183760100 -7200
# Node ID 0886e5861766806aa566f274ed677c9cc1a9770a
# Parent  32ee8cac5c0283ec5b5695d7e8a5dc6d5632df82
tuned;

diff -r 32ee8cac5c02 -r 0886e5861766 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat Jul 07 00:14:59 2007 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sat Jul 07 00:15:00 2007 +0200
@@ -239,8 +239,9 @@
         (if end_state = "" then [] else [Pretty.str end_state]))
   end;
 
-val print_state_context = Pretty.writelns o pretty_state_context;
-fun print_state_default prf_only state = Pretty.writelns (pretty_state prf_only state);
+val print_state_context = Pretty.writeln o Pretty.chunks o pretty_state_context;
+fun print_state_default prf_only state =
+  Pretty.writeln (Pretty.chunks (pretty_state prf_only state));
 
 val print_state_fn = ref print_state_default;
 fun print_state prf_only state = ! print_state_fn prf_only state;