Ide_intf : change type of location in ide

 We use (int * int) option instead of Loc.t, it's easier to use
 later in coqide, and this way we do not depend on camlp4,5

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13929 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 12 insertions, 8 deletions

diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml
index fb8c9e94d3..534f181af8 100644
--- a/toplevel/ide_intf.ml
+++ b/toplevel/ide_intf.ml
@@ -52,9 +52,11 @@ let make_cases s : string list list call =
 
 (** * Coq answers to CoqIde *)
 
+type location = (int * int) option (* start and end of the error *)
+
 type 'a value =
   | Good of 'a
-  | Fail of (Util.loc option * string)
+  | Fail of (location * string)
 
 type handler = {
   is_in_loadpath : string -> bool;
diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli
index 2550a30cd3..42d1a943ac 100644
--- a/toplevel/ide_intf.mli
+++ b/toplevel/ide_intf.mli
@@ -27,9 +27,11 @@ val read_stdout : string call
 
 (** * Coq answers to CoqIde *)
 
+type location = (int * int) option (* start and end of the error *)
+
 type 'a value =
   | Good of 'a
-  | Fail of (Util.loc option * string)
+  | Fail of (location * string)
 
 type handler = {
   is_in_loadpath : string -> bool;
@@ -43,5 +45,5 @@ type handler = {
 }
 
 val abstract_eval_call :
-  handler -> (exn -> Util.loc option * string) ->
+  handler -> (exn -> location * string) ->
   'a call -> 'a value
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 5a51471aaf..0c9a1e79db 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -494,9 +494,9 @@ let explain_exn e =
   let toploc,exc =
     match e with
       | Loc.Exc_located (loc, inner) ->
-          (if loc = dummy_loc then None else Some loc),inner
-      | Error_in_file (s, (is_in_lib, fname, loc), inner) ->
-          None,inner
+	let l = if loc = dummy_loc then None else Some (Util.unloc loc) in
+	l,inner
+      | Error_in_file (s, _, inner) -> None,inner
       | _ -> None,e
   in
   toploc,(Cerrors.explain_exn exc)
@@ -505,10 +505,10 @@ let eval_call c =
   let rec handle_exn = function
     | Vernac.DuringCommandInterp (loc,inner) -> handle_exn inner
     | Vernacexpr.Drop -> None, "Drop is not allowed by coqide!"
-    | Vernacexpr.Quit -> raise Vernacexpr.Quit
+    | Vernacexpr.Quit -> None, "Quit is not allowed by coqide!"
     | e ->
       let (l,pp) = explain_exn e in
-      l,string_of_ppcmds pp
+      l, string_of_ppcmds pp
   in
   let handler = {
     Ide_intf.is_in_loadpath = is_in_loadpath;