# HG changeset patch
# User wenzelm
# Date 935001628 -7200
# Node ID 32a867ed94545a4c41fab58e672497a46f260b88
# Parent  d55cd903c93da4b150370274f904f9d95edcf8f8
proper writeln of begin_state;

diff -r d55cd903c93d -r 32a867ed9454 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Wed Aug 18 20:39:41 1999 +0200
+++ b/src/Pure/goals.ML	Wed Aug 18 20:40:28 1999 +0200
@@ -319,9 +319,12 @@
 val current_goals_markers = ref ("", "", "");
 
 fun print_current_goals_default n max th =
-  let val ref (begin_state, end_state, begin_goal) = current_goals_markers;
-      val ngoals = nprems_of th in
-    writeln (begin_state ^ "Level " ^ string_of_int n ^
+  let
+    val ref (begin_state, end_state, begin_goal) = current_goals_markers;
+    val ngoals = nprems_of th;
+  in
+    if begin_state = "" then () else writeln begin_state;
+    writeln ("Level " ^ string_of_int n ^
       (if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^
         (if ngoals <> 1 then "s" else "") ^ ")"
       else ""));