diff options
Diffstat (limited to 'proofs/tactic_debug.ml')
-rw-r--r-- | proofs/tactic_debug.ml | 5 |
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 (); |