diff --git a/CHANGES.md b/CHANGES.md index 7822040b..64fd531e 100644 --- a/CHANGES.md +++ b/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 ------------------------------- diff --git a/controller/rq_common.ml b/controller/rq_common.ml index 048ccbd3..d1a25be0 100644 --- a/controller/rq_common.ml +++ b/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 diff --git a/examples/unicode2.v b/examples/unicode2.v new file mode 100644 index 00000000..2f30636c --- /dev/null +++ b/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.