# HG changeset patch
# User lcp
# Date 751220401 -3600
# Node ID 8380bc0adde7e5a793cddfb76a60daa37b034af7
# Parent  1b14cd9237726700730bd1d500e4d342aa56646c
Pure/drule/print_goals_ref: new, for Centaur interface
Pure/tctical/tracify,print_tac: now call !print_goals_ref
Pure/goals/print_top,prepare_proof: now call !print_goals_ref

diff -r 1b14cd923772 -r 8380bc0adde7 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Oct 21 17:10:15 1993 +0100
+++ b/src/Pure/drule.ML	Thu Oct 21 17:20:01 1993 +0100
@@ -36,6 +36,7 @@
   val print_cterm: Sign.cterm -> unit
   val print_ctyp: Sign.ctyp -> unit
   val print_goals: int -> thm -> unit
+  val print_goals_ref: (int -> thm -> unit) ref
   val print_sg: Sign.sg -> unit
   val print_theory: theory -> unit
   val pprint_sg: Sign.sg -> pprint_args -> unit
@@ -332,6 +333,8 @@
    printff tpairs
 end;
 
+(*"hook" for user interfaces: allows print_goals to be replaced*)
+val print_goals_ref = ref print_goals;
 
 (** theorem equality test is exported and used by BEST_FIRST **)
 
diff -r 1b14cd923772 -r 8380bc0adde7 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Thu Oct 21 17:10:15 1993 +0100
+++ b/src/Pure/tctical.ML	Thu Oct 21 17:20:01 1993 +0100
@@ -179,8 +179,9 @@
 val goals_limit = ref 10;
 
 (*Print the current proof state and pass it on.*)
-val print_tac = Tactic (fn state => 
-  (print_goals (!goals_limit) state;   Sequence.single state));
+val print_tac = Tactic 
+    (fn state => 
+     (!print_goals_ref (!goals_limit) state;   Sequence.single state));
 
 (*Pause until a line is typed -- if non-empty then fail. *)
 val pause_tac = Tactic (fn state => 
@@ -210,7 +211,7 @@
 
 (*Extract from a tactic, a thm->thm seq function that handles tracing*)
 fun tracify flag (Tactic tf) state =
-  if !flag then (print_goals (!goals_limit) state;  
+  if !flag then (!print_goals_ref (!goals_limit) state;  
 		 prs"** Press RETURN to continue: ";
 		 exec_trace_command flag (tf,state))
   else tf state;