# HG changeset patch
# User wenzelm
# Date 980975753 -3600
# Node ID 14b78c0c9f0589df1187eb802114ba7e2bc73cfc
# Parent  2c6559297be3fc1b444f87b8f7c003db4c71f60c
pretty_text: tweak_lines handles linebreaks gracefully;

diff -r 2c6559297be3 -r 14b78c0c9f05 src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Wed Jan 31 22:14:53 2001 +0100
+++ b/src/Pure/Isar/isar_output.ML	Wed Jan 31 22:15:53 2001 +0100
@@ -279,8 +279,10 @@
     Pretty.str_of prt
     |> enclose "\\isa{" "}";
 
+fun tweak_line s =
+  if ! display then s else Symbol.strip_blanks s;
 
-val pretty_text = Pretty.chunks o map Pretty.str o Library.split_lines;
+val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines;
 
 val pretty_source =
   pretty_text o space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;