summaryrefslogtreecommitdiff
path: root/proofs/tactic_debug.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/tactic_debug.ml')
-rw-r--r--proofs/tactic_debug.ml5
1 files changed, 3 insertions, 2 deletions
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 43807872..889e06a8 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -76,11 +76,12 @@ let rec prompt level =
begin
msg (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ");
flush stdout;
- let inst = read_line () in
+ let exit () = skip:=0;allskip:=0;raise Sys.Break in
+ let inst = try read_line () with End_of_file -> exit () in
match inst with
| "" -> true
| "s" -> false
- | "x" -> print_char (Char.chr 8);skip:=0;allskip:=0;raise Sys.Break
+ | "x" -> print_char (Char.chr 8); exit ()
| "h"| "?" ->
begin
help ();