# HG changeset patch
# User oheimb
# Date 916413211 -3600
# Node ID 4f224fd882f9bf8905d389693c7c29755c0f3ee4
# Parent  6f049245afadfc4e4f0fcda0b2f3e32cb4bf377f
removed empty line (in case of empty begin_state marker) before Level line
added printing of subgoals number in Level line

diff -r 6f049245afad -r 4f224fd882f9 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Thu Jan 14 14:39:11 1999 +0100
+++ b/src/Pure/goals.ML	Fri Jan 15 16:13:31 1999 +0100
@@ -309,9 +309,11 @@
 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 in
-    if begin_state = "" then () else writeln begin_state;
-    writeln ("Level " ^ string_of_int n);
+  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 ^ 
+	" (" ^ string_of_int ngoals ^ " subgoal" ^ 
+	   (if ngoals > 1 then "s" else "") ^ ")");
     Locale.print_goals_marker begin_goal max th;
     if end_state = "" then () else writeln end_state
   end;