# HG changeset patch # User wenzelm # Date 1187635439 -7200 # Node ID 44556727197ab441a71b28c299ef225ee679485b # Parent d75af3e90e82a137cc0f82e0218abc9c244d8541 TextIO.inputLine: non-critical (assume exclusive ownership); diff -r d75af3e90e82 -r 44556727197a src/Pure/tctical.ML --- a/src/Pure/tctical.ML Mon Aug 20 20:43:58 2007 +0200 +++ b/src/Pure/tctical.ML Mon Aug 20 20:43:59 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 CRITICAL (fn () => TextIO.inputLine TextIO.stdIn) = SOME "\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,7 +215,7 @@ (*Handle all tracing commands for current state and tactic *) fun exec_trace_command flag (tac, st) = - case CRITICAL (fn () => TextIO.inputLine TextIO.stdIn) of + case TextIO.inputLine TextIO.stdIn of SOME "\n" => tac st | SOME "f\n" => Seq.empty | SOME "o\n" => (flag:=false; tac st)