# HG changeset patch # User paulson # Date 914860171 -3600 # Node ID 684ec6a1d8028414478bb27ff9a18502d1463bb8 # Parent bd37dc0f56d971dfbaf1eccace4e24cc9451c598 Added a "message" argument to print_tac diff -r bd37dc0f56d9 -r 684ec6a1d802 src/Pure/tctical.ML --- a/src/Pure/tctical.ML Mon Dec 28 16:48:59 1998 +0100 +++ b/src/Pure/tctical.ML Mon Dec 28 16:49:31 1998 +0100 @@ -38,7 +38,7 @@ val ORELSE : tactic * tactic -> tactic val ORELSE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic val pause_tac : tactic - val print_tac : tactic + val print_tac : string -> tactic val REPEAT : tactic -> tactic val REPEAT1 : tactic -> tactic val REPEAT_DETERM_N : int -> tactic -> tactic @@ -192,9 +192,10 @@ val goals_limit = ref 10; (*Print the current proof state and pass it on.*) -val print_tac = +fun print_tac msg = (fn st => - (print_goals (!goals_limit) st; Seq.single st)); + (writeln msg; + print_goals (!goals_limit) st; Seq.single st)); (*Pause until a line is typed -- if non-empty then fail. *) fun pause_tac st =