--- a/src/Pure/tctical.ML Wed May 30 23:32:54 2007 +0200
+++ b/src/Pure/tctical.ML Thu May 31 01:25:24 2007 +0200
@@ -203,7 +203,7 @@
(*Pause until a line is typed -- if non-empty then fail. *)
fun pause_tac st =
(tracing "** Press RETURN to continue:";
- if TextIO.inputLine TextIO.stdIn = "\n" then Seq.single st
+ if TextIO.inputLine TextIO.stdIn = SOME "\n" then Seq.single st
else (tracing "Goodbye"; Seq.empty));
exception TRACE_EXIT of thm
@@ -215,13 +215,13 @@
(*Handle all tracing commands for current state and tactic *)
fun exec_trace_command flag (tac, st) =
- case TextIO.inputLine(TextIO.stdIn) of
- "\n" => tac st
- | "f\n" => Seq.empty
- | "o\n" => (flag:=false; tac st)
- | "s\n" => (suppress_tracing:=true; tac st)
- | "x\n" => (tracing "Exiting now"; raise (TRACE_EXIT st))
- | "quit\n" => raise TRACE_QUIT
+ case TextIO.inputLine TextIO.stdIn of
+ SOME "\n" => tac st
+ | SOME "f\n" => Seq.empty
+ | SOME "o\n" => (flag:=false; tac st)
+ | SOME "s\n" => (suppress_tracing:=true; tac st)
+ | SOME "x\n" => (tracing "Exiting now"; raise (TRACE_EXIT st))
+ | SOME "quit\n" => raise TRACE_QUIT
| _ => (tracing
"Type RETURN to continue or...\n\
\ f - to fail here\n\