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

7 files changed, 19 insertions, 15 deletions

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index 70bc4d1cd1..d843f9ac51 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -115,7 +115,7 @@ object(self)
                    | Ide_intf.Good results ->
                        ("Result for command " ^ phrase ^ ":\n" ^ results))
       with e ->
-	let (s,loc) = Coq.process_exn e in
+	let (_,s) = Coq.process_exn e in
 	assert (Glib.Utf8.validate s);
 	result#buffer#set_text s
     in
diff --git a/ide/coq.ml b/ide/coq.ml
index 41c9546d1f..96048c3b30 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -211,8 +211,8 @@ end
 
 let process_exn = function
   | End_of_file ->
-    "Warning: End_of_file occurred (possibly a forced restart of coqtop)", None
-  | e -> Printexc.to_string e,None
+    None, "Warning: End_of_file occurred (possibly a forced restart of coqtop)"
+  | e -> None, Printexc.to_string e
 
 let goals coqtop =
   match PrintOpt.enforce_hack coqtop with
diff --git a/ide/coq.mli b/ide/coq.mli
index a96ed31c76..148840be26 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -23,7 +23,7 @@ val coqtop_zombies : unit -> int
 
 val reset_coqtop : coqtop -> unit
 
-val process_exn : exn -> string*(Util.loc option)
+val process_exn : exn -> Ide_intf.location * string
 
 module PrintOpt :
 sig
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 1797a7e51a..e553ca0b46 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -803,7 +803,7 @@ object(self)
   method send_to_coq verbosely replace phrase show_output show_error localize =
     let display_output msg =
       self#insert_message (if show_output then msg else "") in
-    let display_error (s,loc) =
+    let display_error (loc,s) =
       if show_error then begin
         if not (Glib.Utf8.validate s) then
           flash_info "This error is so nasty that I can't even display it." 
@@ -811,7 +811,7 @@ object(self)
           self#insert_message s;
           message_view#misc#draw None;
           if localize then
-            (match Option.map Util.unloc loc with
+            (match loc with
                | None -> ()
                | Some (start,stop) ->
                    let convert_pos = byte_offset_to_char_offset phrase in
@@ -830,7 +830,7 @@ object(self)
       full_goal_done <- false;
       prerr_endline "Send_to_coq starting now";
       match Coq.interp mycoqtop verbosely phrase with
-        | Ide_intf.Fail (l,str) -> sync display_error (str,l); None
+        | Ide_intf.Fail (l,str) -> sync display_error (l,str); None
         | Ide_intf.Good r ->
             match Coq.read_stdout mycoqtop with
               | Ide_intf.Fail (_,str) ->
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;