diff options
author | Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
commit | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (patch) | |
tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /toplevel/ide_intf.ml | |
parent | bf12eb93f3f6a6a824a10878878fadd59745aae0 (diff) |
Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg
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) |