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
--- 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 **)
--- 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;