From 213e86842db2cdc3acc8cdf6d28f46c7ebaec5d4 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Mon, 9 May 2016 14:46:11 +0200
Subject: Use the actual location of an error in the error pane (bug #4169).

A "sentence" includes all the blank lines and all the comments that
precede a command. So its starting location might be far from any error it
contains. This patch changes error reporting so that it relies on the
location of errors rather than the location of erroneous sentences.
---
 ide/coqOps.ml | 24 +++++++++++++++++-------
 1 file changed, 17 insertions(+), 7 deletions(-)

(limited to 'ide/coqOps.ml')

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 850b41e59..f3ae317a3 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -12,7 +12,9 @@ open Ideutils
 open Interface
 open Feedback
 
-type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of string ]
+let b2c = byte_offset_to_char_offset
+
+type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of Loc.t * string ]
 type mem_flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR ]
 let mem_flag_of_flag : flag -> mem_flag = function
   | `ERROR _ -> `ERROR
@@ -397,8 +399,8 @@ object(self)
     let start_sentence, stop_sentence, phrase = self#get_sentence sentence in
     let pre_chars, post_chars =
       if Loc.is_ghost loc then 0, String.length phrase else Loc.unloc loc in
-    let pre = Ideutils.glib_utf8_pos_to_offset phrase ~off:pre_chars in
-    let post = Ideutils.glib_utf8_pos_to_offset phrase ~off:post_chars in
+    let pre = b2c phrase pre_chars in
+    let post = b2c phrase post_chars in
     let start = start_sentence#forward_chars pre in
     let stop = start_sentence#forward_chars post in
     let markup = Glib.Markup.escape_text text in
@@ -462,7 +464,7 @@ object(self)
       | ErrorMsg(loc, msg), Some (id,sentence) ->
           log "ErrorMsg" id;
           remove_flag sentence `PROCESSING;
-          add_flag sentence (`ERROR msg);
+          add_flag sentence (`ERROR (loc, msg));
           self#mark_as_needed sentence;
           self#attach_tooltip sentence loc msg;
           if not (Loc.is_ghost loc) then
@@ -501,8 +503,8 @@ object(self)
     | None -> ()
     | Some (start, stop) ->
         buffer#apply_tag Tags.Script.error
-          ~start:(iter#forward_chars (byte_offset_to_char_offset phrase start))
-          ~stop:(iter#forward_chars (byte_offset_to_char_offset phrase stop))
+          ~start:(iter#forward_chars (b2c phrase start))
+          ~stop:(iter#forward_chars (b2c phrase stop))
 
   method private position_error_tag_at_sentence sentence loc =
     let start, _, phrase = self#get_sentence sentence in
@@ -653,7 +655,15 @@ object(self)
   method get_errors =
     let extract_error s =
       match List.find (function `ERROR _ -> true | _ -> false) s.flags with
-      | `ERROR msg -> (buffer#get_iter_at_mark s.start)#line + 1, msg
+      | `ERROR (loc, msg) ->
+         let iter =
+           if Loc.is_ghost loc then
+             buffer#get_iter_at_mark s.start
+           else
+             let (iter, _, phrase) = self#get_sentence s in
+             let (start, _) = Loc.unloc loc in
+             iter#forward_chars (b2c phrase start) in
+         iter#line + 1, msg
       | _ -> assert false in
     List.rev
       (Doc.fold_all document [] (fun acc _ _ s ->
-- 
cgit v1.2.3