diff options
author | 2016-06-27 11:03:43 +0200 | |
---|---|---|
committer | 2016-07-03 12:08:03 +0200 | |
commit | f14b6f1a17652566f0cbc00ce81421ba0684dad5 (patch) | |
tree | 8a331593d0d1b518e8764c92ac54e3b11c222358 /ide | |
parent | 500d38d0887febb614ddcadebaef81e0c7942584 (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.ml | 14 | ||||
-rw-r--r-- | ide/xmlprotocol.ml | 2 |
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 *) |