# 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)