fixing error message display.

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

5 files changed, 26 insertions, 26 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index cb9d5b8959..751591f793 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -81,14 +81,14 @@ let version () =
     (if Mltop.is_native then "native" else "bytecode")
     (if Coq_config.best="opt" then "native" else "bytecode")
 
-exception Coq_failure of (Util.loc * Pp.std_ppcmds)
+exception Coq_failure of (Util.loc option * string)
 
 let eval_call coqtop (c:'a Ide_blob.call) =
   Safe_marshal.send coqtop.cin c;
   let res = (Safe_marshal.receive: in_channel -> 'a Ide_blob.value) coqtop.cout in
   match res with
     | Ide_blob.Good v -> v
-    | Ide_blob.Fail (l,pp) -> prerr_endline (msg pp); raise (Coq_failure (l,pp))
+    | Ide_blob.Fail err -> raise (Coq_failure err)
 
 let is_in_loadpath coqtop s = eval_call coqtop (Ide_blob.is_in_loadpath s)
  
diff --git a/ide/coq.mli b/ide/coq.mli
index 926919f70f..b2efd63fcc 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -25,7 +25,7 @@ val kill_coqtop : coqtop -> unit
 
 val reset_coqtop : coqtop -> unit
 
-exception Coq_failure of (Util.loc * Pp.std_ppcmds)
+exception Coq_failure of (Util.loc option * string)
 
 module PrintOpt :
 sig
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 4266d6fb31..c838e603ef 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -770,8 +770,8 @@ 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 e =
-      let (s,loc) = Coq.process_exn e in
+    let display_error (s,loc) =
+      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." 
         else begin
@@ -791,20 +791,21 @@ object(self)
                      ~start:starti
                      ~stop:stopi;
                    input_buffer#place_cursor starti)
-        end in
-      try
-        full_goal_done <- false;
-        prerr_endline "Send_to_coq starting now";
-        let r = Coq.interp mycoqtop verbosely phrase in
-        let is_complete = true in
-        let msg = Coq.read_stdout mycoqtop in
-        sync display_output msg;
-        Some (is_complete,r)
-      with
-        | Coq_failure (l,pp) -> Pervasives.prerr_endline (Coq.msgnl pp); None
-        | e ->
-        if show_error then sync display_error e;
-        None
+        end
+      end in
+    try
+      full_goal_done <- false;
+      prerr_endline "Send_to_coq starting now";
+      let r = Coq.interp mycoqtop verbosely phrase in
+      let is_complete = true in
+      let msg = Coq.read_stdout mycoqtop in
+      sync display_output msg;
+      Some (is_complete,r)
+    with
+      | Coq_failure (l,s) ->
+          sync display_error (s,l); None
+      | e ->
+          sync display_error (Coq.process_exn e); None
 
   method find_phrase_starting_at (start:GText.iter) =
     try
diff --git a/toplevel/ide_blob.ml b/toplevel/ide_blob.ml
index 81ad61930f..b4173f0ca9 100644
--- a/toplevel/ide_blob.ml
+++ b/toplevel/ide_blob.ml
@@ -502,10 +502,10 @@ let explain_exn e =
   let toploc,exc =
     match e with
       | Loc.Exc_located (loc, inner) ->
-          loc,inner
+          (if loc = dummy_loc then None else Some loc),inner
       | Error_in_file (s, (is_in_lib, fname, loc), inner) ->
-          dummy_loc,inner
-      | _ -> dummy_loc,e
+          None,inner
+      | _ -> None,e
   in
   toploc,(Cerrors.explain_exn exc)
 
@@ -527,7 +527,7 @@ type 'a call =
 
 type 'a value =
   | Good of 'a
-  | Fail of (Util.loc * Pp.std_ppcmds)
+  | Fail of (Util.loc option * string)
 
 let eval_call c = 
   let null_formatter = Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ()) in
@@ -549,8 +549,7 @@ let eval_call c =
   with e ->
     let (l,pp) = explain_exn (filter_compat_exn e) in
     (* force evaluation of format stream *)
-    Pp.msg_with null_formatter pp;
-    Fail (l,pp)
+    Fail (l,string_of_ppcmds pp)
 
 let is_in_loadpath s : bool call =
   In_loadpath s
diff --git a/toplevel/ide_blob.mli b/toplevel/ide_blob.mli
index 561821b563..7a34680d1e 100644
--- a/toplevel/ide_blob.mli
+++ b/toplevel/ide_blob.mli
@@ -23,7 +23,7 @@ type 'a call
 
 type 'a value =
   | Good of 'a
-  | Fail of (Util.loc * Pp.std_ppcmds)
+  | Fail of (Util.loc option * string)
 
 val eval_call : 'a call -> 'a value