equal
deleted
inserted
replaced
190 val goals_limit = ref 10; |
190 val goals_limit = ref 10; |
191 |
191 |
192 (*Print the current proof state and pass it on.*) |
192 (*Print the current proof state and pass it on.*) |
193 val print_tac = |
193 val print_tac = |
194 (fn st => |
194 (fn st => |
195 (!print_goals_ref (!goals_limit) st; Sequence.single st)); |
195 (print_goals (!goals_limit) st; Sequence.single st)); |
196 |
196 |
197 (*Pause until a line is typed -- if non-empty then fail. *) |
197 (*Pause until a line is typed -- if non-empty then fail. *) |
198 fun pause_tac st = |
198 fun pause_tac st = |
199 (prs"** Press RETURN to continue: "; |
199 (prs"** Press RETURN to continue: "; |
200 if TextIO.inputLine TextIO.stdIn = "\n" then Sequence.single st |
200 if TextIO.inputLine TextIO.stdIn = "\n" then Sequence.single st |
227 |
227 |
228 |
228 |
229 (*Extract from a tactic, a thm->thm seq function that handles tracing*) |
229 (*Extract from a tactic, a thm->thm seq function that handles tracing*) |
230 fun tracify flag tac st = |
230 fun tracify flag tac st = |
231 if !flag andalso not (!suppress_tracing) |
231 if !flag andalso not (!suppress_tracing) |
232 then (!print_goals_ref (!goals_limit) st; |
232 then (print_goals (!goals_limit) st; |
233 prs"** Press RETURN to continue: "; |
233 prs"** Press RETURN to continue: "; |
234 exec_trace_command flag (tac,st)) |
234 exec_trace_command flag (tac,st)) |
235 else tac st; |
235 else tac st; |
236 |
236 |
237 (*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*) |
237 (*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*) |