equal
deleted
inserted
replaced
201 Seq.single st)); |
201 Seq.single st)); |
202 |
202 |
203 (*Pause until a line is typed -- if non-empty then fail. *) |
203 (*Pause until a line is typed -- if non-empty then fail. *) |
204 fun pause_tac st = |
204 fun pause_tac st = |
205 (tracing "** Press RETURN to continue:"; |
205 (tracing "** Press RETURN to continue:"; |
206 if TextIO.inputLine TextIO.stdIn = SOME "\n" then Seq.single st |
206 if CRITICAL (fn () => TextIO.inputLine TextIO.stdIn) = SOME "\n" then Seq.single st |
207 else (tracing "Goodbye"; Seq.empty)); |
207 else (tracing "Goodbye"; Seq.empty)); |
208 |
208 |
209 exception TRACE_EXIT of thm |
209 exception TRACE_EXIT of thm |
210 and TRACE_QUIT; |
210 and TRACE_QUIT; |
211 |
211 |
213 val trace_REPEAT= ref false |
213 val trace_REPEAT= ref false |
214 and suppress_tracing = ref false; |
214 and suppress_tracing = ref false; |
215 |
215 |
216 (*Handle all tracing commands for current state and tactic *) |
216 (*Handle all tracing commands for current state and tactic *) |
217 fun exec_trace_command flag (tac, st) = |
217 fun exec_trace_command flag (tac, st) = |
218 case TextIO.inputLine TextIO.stdIn of |
218 case CRITICAL (fn () => TextIO.inputLine TextIO.stdIn) of |
219 SOME "\n" => tac st |
219 SOME "\n" => tac st |
220 | SOME "f\n" => Seq.empty |
220 | SOME "f\n" => Seq.empty |
221 | SOME "o\n" => (flag:=false; tac st) |
221 | SOME "o\n" => (flag:=false; tac st) |
222 | SOME "s\n" => (suppress_tracing:=true; tac st) |
222 | SOME "s\n" => (suppress_tracing:=true; tac st) |
223 | SOME "x\n" => (tracing "Exiting now"; raise (TRACE_EXIT st)) |
223 | SOME "x\n" => (tracing "Exiting now"; raise (TRACE_EXIT st)) |