Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
TextIO.inputLine: non-critical (assume exclusive ownership);
authorwenzelm
Mon, 20 Aug 2007 20:43:59 +0200
changeset 24359 44556727197a
parent 24358 d75af3e90e82
child 24360 a0da34cc081c
TextIO.inputLine: non-critical (assume exclusive ownership);
src/Pure/tctical.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle