summaryrefslogtreecommitdiff
path: root/toplevel/ide_slave.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/ide_slave.ml')
-rw-r--r--toplevel/ide_slave.ml11
1 files changed, 6 insertions, 5 deletions
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index d67b272e..6e9a0ee0 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -237,7 +237,7 @@ let status () =
in
let proof =
try Some (Names.string_of_id (Proof_global.get_current_proof_name ()))
- with _ -> None
+ with Proof_global.NoCurrentProof -> None
in
let allproofs =
let l = Proof_global.get_all_proof_names () in
@@ -259,7 +259,8 @@ let search flags =
| (Interface.Name_Pattern s, b) :: l ->
let regexp =
try Str.regexp s
- with _ -> Util.error ("Invalid regexp: " ^ s)
+ with e when Errors.noncritical e ->
+ Util.error ("Invalid regexp: " ^ s)
in
extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l
| (Interface.Type_Pattern s, b) :: l ->
@@ -454,12 +455,12 @@ let loop () =
Xml_utils.print_xml !orig_stdout xml_answer;
flush !orig_stdout
done
- with e ->
- let msg = Printexc.to_string e in
+ with any ->
+ let msg = Printexc.to_string any in
let r = "Fatal exception in coqtop:\n" ^ msg in
pr_debug ("==> " ^ r);
(try
Xml_utils.print_xml !orig_stdout (fail r);
flush !orig_stdout
- with _ -> ());
+ with any -> ());
exit 1