# HG changeset patch
# User wenzelm
# Date 909667963 -3600
# Node ID cbd439ed350d33a82188cf845eb9a2d1a118347e
# Parent  c675d4a8c26aba57ac6e212e008fb99f6d0dea53
tuned current_goals_markers semantics to avoid empty lines;

diff -r c675d4a8c26a -r cbd439ed350d src/Pure/goals.ML
--- a/src/Pure/goals.ML	Thu Oct 29 12:42:33 1998 +0100
+++ b/src/Pure/goals.ML	Thu Oct 29 14:32:43 1998 +0100
@@ -279,10 +279,10 @@
 
 fun print_current_goals_default n max th =
   let val ref (begin_state, end_state, begin_goal) = current_goals_markers in
-    writeln begin_state;
+    if begin_state = "" then () else writeln begin_state;
     writeln ("Level " ^ string_of_int n);
     Locale.print_goals_marker begin_goal max th;
-    writeln end_state
+    if end_state = "" then () else writeln end_state
   end;
 
 val print_current_goals_fn = ref print_current_goals_default;