aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-06-27 11:03:43 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-07-03 12:08:03 +0200
commitf14b6f1a17652566f0cbc00ce81421ba0684dad5 (patch)
tree8a331593d0d1b518e8764c92ac54e3b11c222358 /ide
parent500d38d0887febb614ddcadebaef81e0c7942584 (diff)
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
Diffstat (limited to 'ide')
-rw-r--r--ide/ide_slave.ml14
-rw-r--r--ide/xmlprotocol.ml2
2 files changed, 8 insertions, 8 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 86e09922c..4046ef7ae 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -8,7 +8,7 @@
(************************************************************************)
open Vernacexpr
-open Errors
+open CErrors
open Util
open Pp
open Printer
@@ -96,7 +96,7 @@ let is_undo cmd = match cmd with
(** Check whether a command is forbidden by CoqIDE *)
let coqide_cmd_checks (loc,ast) =
- let user_error s = Errors.user_err_loc (loc, "CoqIde", str s) in
+ let user_error s = CErrors.user_err_loc (loc, "CoqIde", str s) in
if is_debug ast then
user_error "Debug mode not available within CoqIDE";
if is_known_option ast then
@@ -300,7 +300,7 @@ let dirpath_of_string_list s =
let id =
try Nametab.full_name_module qid
with Not_found ->
- Errors.errorlabstrm "Search.interface_search"
+ CErrors.errorlabstrm "Search.interface_search"
(str "Module " ++ str path ++ str " not found.")
in
id
@@ -365,12 +365,12 @@ let handle_exn (e, info) =
| _ -> None in
let mk_msg () =
let msg = read_stdout () in
- let msg = str msg ++ fnl () ++ Errors.print ~info e in
+ let msg = str msg ++ fnl () ++ CErrors.print ~info e in
Richpp.richpp_of_pp msg
in
match e with
- | Errors.Drop -> dummy, None, Richpp.richpp_of_string "Drop is not allowed by coqide!"
- | Errors.Quit -> dummy, None, Richpp.richpp_of_string "Quit is not allowed by coqide!"
+ | CErrors.Drop -> dummy, None, Richpp.richpp_of_string "Drop is not allowed by coqide!"
+ | CErrors.Quit -> dummy, None, Richpp.richpp_of_string "Quit is not allowed by coqide!"
| e ->
match Stateid.get info with
| Some (valid, _) -> valid, loc_of info, mk_msg ()
@@ -469,7 +469,7 @@ let print_xml =
fun oc xml ->
Mutex.lock m;
try Xml_printer.print oc xml; Mutex.unlock m
- with e -> let e = Errors.push e in Mutex.unlock m; iraise e
+ with e -> let e = CErrors.push e in Mutex.unlock m; iraise e
let slave_logger xml_oc ?loc level message =
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index 79509fe02..aecb317bc 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -607,7 +607,7 @@ let abstract_eval_call : type a. _ -> a call -> a value = fun handler c ->
| PrintAst x -> mkGood (handler.print_ast x)
| Annotate x -> mkGood (handler.annotate x)
with any ->
- let any = Errors.push any in
+ let any = CErrors.push any in
Fail (handler.handle_exn any)
(** brain dead code, edit if protocol messages are added/removed *)