diff options
Diffstat (limited to 'toplevel/ide_intf.ml')
| -rw-r--r-- | toplevel/ide_intf.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml index 28f97dc8..6937eeb8 100644 --- a/toplevel/ide_intf.ml +++ b/toplevel/ide_intf.ml @@ -89,8 +89,8 @@ let abstract_eval_call handler c = | Quit -> Obj.magic (handler.quit () : unit) | About -> Obj.magic (handler.about () : coq_info) in Good res - with e -> - let (l, str) = handler.handle_exn e in + with any -> + let (l, str) = handler.handle_exn any in Fail (l,str) (** * XML data marshalling *) @@ -275,7 +275,7 @@ let to_value f = function let loc_s = int_of_string (List.assoc "loc_s" attrs) in let loc_e = int_of_string (List.assoc "loc_e" attrs) in Some (loc_s, loc_e) - with _ -> None + with e when e <> Sys.Break -> None in let msg = raw_string l in Fail (loc, msg) |