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

4 files changed, 7 insertions, 7 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) ->