# HG changeset patch
# User wenzelm
# Date 909079662 -7200
# Node ID 5d66410cceae26b696faa4d976a54b32454e03a4
# Parent  1d1175ef2d560efb2a865b3344bd59f400bc6089
support current_goals_markers ref variable for print_current_goals;

diff -r 1d1175ef2d56 -r 5d66410cceae src/Pure/goals.ML
--- a/src/Pure/goals.ML	Thu Oct 22 12:35:40 1998 +0200
+++ b/src/Pure/goals.ML	Thu Oct 22 20:07:42 1998 +0200
@@ -42,6 +42,7 @@
   val goal		: theory -> string -> thm list
   val goalw		: theory -> thm list -> string -> thm list
   val goalw_cterm	: thm list -> cterm -> thm list
+  val current_goals_markers: (string * string * string) ref
   val print_current_goals_default: (int -> int -> thm -> unit)
   val print_current_goals_fn : (int -> int -> thm -> unit) ref
   val pop_proof		: unit -> thm list
@@ -271,8 +272,15 @@
 
 
 (*Print goals of current level*)
+val current_goals_markers = ref ("", "", "");
+
 fun print_current_goals_default n max th =
-  (writeln ("Level " ^ string_of_int n); print_goals max th);
+  let val ref (begin_state, end_state, begin_goal) = current_goals_markers in
+    writeln begin_state;
+    writeln ("Level " ^ string_of_int n);
+    Locale.print_goals_marker begin_goal max th;
+    writeln end_state
+  end;
 
 val print_current_goals_fn = ref print_current_goals_default;
 
diff -r 1d1175ef2d56 -r 5d66410cceae src/Pure/locale.ML
--- a/src/Pure/locale.ML	Thu Oct 22 12:35:40 1998 +0200
+++ b/src/Pure/locale.ML	Thu Oct 22 20:07:42 1998 +0200
@@ -19,6 +19,7 @@
 sig
   val print_locales: theory -> unit
   val print_goals: int -> thm -> unit
+  val print_goals_marker: string -> int -> thm -> unit
 end;
 
 signature LOCALE =
@@ -476,7 +477,7 @@
 
 in
 
-  fun print_goals maxgoals state =
+  fun print_goals_marker begin_goal maxgoals state =
     let
       val {sign, ...} = rep_thm state;
 
@@ -505,7 +506,7 @@
 
       fun print_subgoals (_, []) = ()
         | print_subgoals (n, A :: As) = (Pretty.writeln (Pretty.blk (0,
-            [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A]));
+            [Pretty.str (begin_goal ^ " " ^ string_of_int n ^ ". "), prt_term A]));
               print_subgoals (n + 1, As));
 
       val print_ffpairs =
@@ -540,6 +541,8 @@
      (! show_types orelse ! show_sorts, ! show_sorts)
   end;
 
+  val print_goals = print_goals_marker "";
+
 end;