Merge pull request #597 from ejgallego/hover_unicode

[hover] Fix `get_id_at_point` in the presence of Unicode chars

CHANGES.md

@@ -7,6 +7,9 @@
    mistake (@ejgallego, #588)
  - hover plugins can now access the full document, this is convenient
    for many use cases (@ejgallego, #591)
+ - fix hover position computation on the presence of Utf characters
+   (@ejgallego, #597, thanks to Pierre Courtieu for the report and
+   example, closes #594)
 
 # coq-lsp 0.1.8: Trick-or-treat
 -------------------------------

controller/rq_common.ml

@@ -5,6 +5,7 @@
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
 
+(* XXX: this doesn't work for Unicode either... *)
 (* Common with completion... refactor and make proper *)
 let is_id_char x =
   ('a' <= x && x <= 'z')
@@ -43,5 +44,9 @@ let get_id_at_point ~contents ~point =
   let { Fleche.Contents.lines; _ } = contents in
   if line <= Array.length lines then
     let line = Array.get lines line in
-    if character <= String.length line then find_id line character else None
+    (* XXX UTF this will fail on unicode chars that differ among UTF-8/16 (cc
+       #531) *)
+    match Coq.Utf8.index_of_char ~line ~char:character with
+    | None -> None
+    | Some character -> find_id line character
   else None

examples/unicode2.v

@@ -0,0 +1,7 @@
+(* Thanks to Pierre Courtieu for the example and report *)
+Require Import Utf8.
+
+(* Check hover works properly for `Nopick` *)
+Variant pick_spec (T : Type) (P : T -> Prop) : option T -> Type :=
+  | Pick : forall x : T, P x -> pick_spec T P (Some x)
+  | Nopick : (∀ x : T, ¬ (P x)) → pick_spec T P None.