aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-05-09 14:46:11 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-05-09 14:46:11 +0200
commit213e86842db2cdc3acc8cdf6d28f46c7ebaec5d4 (patch)
tree1e9bb531e72906cd3792f9a6bbca88acd5ade9e8
parent4422432dd55c823595f31163c92306349769d3e4 (diff)
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.
-rw-r--r--ide/coqOps.ml24
1 files changed, 17 insertions, 7 deletions
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 ->