Merge pull request #624 from ineol/hover

[flèche] Store ranges in protocol-native encoding

CHANGES.md

@@ -143,6 +143,8 @@
    (@ejgallgo, #719)
  - Center the view if cursor goes out of scope in
    `sentenceNext/sentencePrevious` (@ejgallego, #718)
+ - Switch Flèche range encoding to protocol native, this means UTF-16
+   for now (Léo Stefanesco, @ejgallego, #624, fixes #620, #621)
 
 # coq-lsp 0.1.8.1: Spring fix
 -----------------------------

CONTRIBUTING.md

@@ -218,6 +218,29 @@ Some tips:
 
 [ocamlformat]: https://github.com/ocaml-ppx/ocamlformat
 
+### Unicode setup
+
+Flèche stores locations in the protocol-native format. This has the
+advantage that conversion is needed only at range creation point
+(where we usually have access to the document to perform the
+conversion).
+
+This way, we can send ranges to the client without conversion.
+
+Request that work on the raw `Contents.t` buffer must do the inverse
+conversion, but we handle this via a proper text API that is aware of
+the conversion.
+
+For now, the setup for Coq is:
+
+- protocol-level (and Flèche) encoding: UTF-16 (due to LSP)
+- `Contents.t`: UTF-8 (sent to Coq)
+
+It would be very easy to set this parameters at initialization time,
+ideal would be for LSP clients to catch up and allow UTF-8 encodings
+(so no conversion is needed, at least for Coq), but it seems that we
+will take a while to get to this point.
+
 ## Client guide (VS Code Extension)
 
 The VS Code extension is setup as a standard `npm` Typescript + React package

controller/rq_common.ml

@@ -44,9 +44,33 @@ 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
-    (* 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
+    let character =
+      Lang.Utf.utf8_offset_of_utf16_offset ~line ~offset:character
+    in
+    find_id line character
   else None
+
+let validate_line ~(contents : Fleche.Contents.t) ~line =
+  if Array.length contents.lines > line then
+    Some (Array.get contents.lines line)
+  else None
+
+let validate_column char line =
+  let length = Lang.Utf.length_utf16 line in
+  if char < length then
+    let char = Lang.Utf.utf8_offset_of_utf16_offset ~line ~offset:char in
+    Some (String.get line char)
+  else None
+
+(* This returns a byte-based char offset for the line *)
+let validate_position ~contents ~point =
+  let line, char = point in
+  validate_line ~contents ~line |> fun l -> Option.bind l (validate_column char)
+
+let get_char_at_point ~contents ~point =
+  let line, char = point in
+  if char >= 1 then
+    let point = (line, char - 1) in
+    validate_position ~contents ~point
+  else (* Can't get previous char *)
+    None

controller/rq_common.mli

@@ -5,5 +5,11 @@
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
 
+(* Contents utils, should be moved to Contents.t , they mainly handle character
+   enconding conversiong between protocol and prover positions, if needed *)
+
 val get_id_at_point :
   contents:Fleche.Contents.t -> point:int * int -> string option
+
+val get_char_at_point :
+  contents:Fleche.Contents.t -> point:int * int -> char option

controller/rq_completion.ml

@@ -70,31 +70,11 @@ let unicode_list point : Yojson.Safe.t list =
   (* Coq's CList.map is tail-recursive *)
   CList.map (mk_unicode_completion_item point) ulist
 
-let validate_line ~(doc : Fleche.Doc.t) ~line =
-  if Array.length doc.contents.lines > line then
-    Some (Array.get doc.contents.lines line)
-  else None
-
-(* This returns a byte-based char offset for the line *)
-let validate_position ~doc ~point =
-  let line, char = point in
-  Option.bind (validate_line ~doc ~line) (fun line ->
-      let char = Coq.Utf8.get_byte_offset_from_utf16_pos line char in
-      Option.bind char (fun index -> Some (String.get line index)))
-
-let get_char_at_point ~(doc : Fleche.Doc.t) ~point =
-  let line, char = point in
-  if char >= 1 then
-    let point = (line, char - 1) in
-    validate_position ~doc ~point
-  else (* Can't get previous char *)
-    None
-
-(* point is a utf char! *)
-let completion ~token:_ ~doc ~point =
+let completion ~token:_ ~(doc : Fleche.Doc.t) ~point =
   (* Instead of get_char_at_point we should have a CompletionContext.t, to be
      addressed in further completion PRs *)
-  (match get_char_at_point ~doc ~point with
+  let contents = doc.contents in
+  (match Rq_common.get_char_at_point ~contents ~point with
   | None ->
     let incomplete = true in
     let items = [] in

controller/rq_hover.ml

@@ -242,7 +242,7 @@ end
 (* Register in-file hover plugins *)
 let () = List.iter Register.add [ Loc_info.h; Stats.h; Type.h; Notation.h ]
 
-let hover ~token ~doc ~point =
+let hover ~token ~(doc : Fleche.Doc.t) ~point =
   let node = Info.LC.node ~doc ~point Exact in
   let range = Option.map Doc.Node.range node in
   let hovers = Register.fire ~token ~doc ~point ~node in

coq/dune

@@ -1,11 +1,8 @@
 (library
  (name coq)
  (public_name coq-lsp.coq)
- ; Unfortunate we have to link the STM due to the LTAC plugin
- ; depending on it, we should fix this upstream
- (inline_tests)
  (preprocess
-  (pps ppx_compare ppx_hash ppx_inline_test))
+  (pps ppx_compare ppx_hash))
  (libraries
   (select
    limits_mp_impl.ml

coq/utils.ml

@@ -16,12 +16,10 @@
 
 (* We convert in case of failure to some default values *)
 
-let char_of_index ~lines ~line ~byte =
+let utf16_offset_of_utf8_offset ~lines ~line ~byte =
   if line < Array.length lines then
     let line = Array.get lines line in
-    match Utf8.char_of_index ~line ~byte with
-    | Some char -> char
-    | None -> Utf8.length line
+    Lang.Utf.utf16_offset_of_utf8_offset ~line ~offset:byte
   else 0
 
 let to_range ~lines (p : Loc.t) : Lang.Range.t =
@@ -34,8 +32,12 @@ let to_range ~lines (p : Loc.t) : Lang.Range.t =
   let start_col = bp - bol_pos in
   let end_col = ep - bol_pos_last in
 
-  let start_col = char_of_index ~lines ~line:start_line ~byte:start_col in
-  let end_col = char_of_index ~lines ~line:end_line ~byte:end_col in
+  let start_col =
+    utf16_offset_of_utf8_offset ~lines ~line:start_line ~byte:start_col
+  in
+  let end_col =
+    utf16_offset_of_utf8_offset ~lines ~line:end_line ~byte:end_col
+  in
   Lang.Range.
     { start = { line = start_line; character = start_col; offset = bp }
     ; end_ = { line = end_line; character = end_col; offset = ep }

examples/unicode1.v

@@ -7,3 +7,8 @@ Goal forall Γ Δ, Γ ⊆ Δ -> P Γ.
 (* check goal is updated after the intros here properly *)
 intros Γ Δ s.
 foo.
+Abort.
+
+Goal forall Γ Δ, Γ ⊆ Δ -> P Γ.
+(* check goal is updated after the intros here properly *)
+intros Γ Δ 𝒞.    foo.

fleche/contents.ml

@@ -142,7 +142,7 @@ let get_last_text text =
   let lines = CString.split_on_char '\n' text |> Array.of_list in
   let n_lines = Array.length lines in
   let last_line = if n_lines < 1 then "" else Array.get lines (n_lines - 1) in
-  let character = Coq.Utf8.length last_line in
+  let character = Lang.Utf.length_utf16 last_line in
   (Lang.Point.{ line = n_lines - 1; character; offset }, lines)
 
 let make ~uri ~raw =

fleche/doc.ml

@@ -1020,9 +1020,7 @@ let loc_after ~lines ~uri (r : Lang.Range.t) =
   let end_index =
     let line = Array.get lines r.end_.line in
     debug_loc_after line r;
-    match Coq.Utf8.index_of_char ~line ~char:r.end_.character with
-    | None -> String.length line
-    | Some index -> index
+    Lang.Utf.utf8_offset_of_utf16_offset ~line ~offset:r.end_.character
   in
   let bol_pos_last = r.end_.offset - end_index in
   { Loc.fname = init_fname ~uri

lang/diagnostic.ml

@@ -1,6 +1,6 @@
 (************************************************************************)
 (* Flèche => document manager: Language Support                         *)
-(* Copyright 2019-2023 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
+(* Copyright 2019-2024 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
 

lang/diagnostic.mli

@@ -1,6 +1,6 @@
 (************************************************************************)
 (* Flèche => document manager: Language Support                         *)
-(* Copyright 2019-2023 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
+(* Copyright 2019-2024 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
 

lang/dune

@@ -1,4 +1,15 @@
 (library
  (name lang)
  (public_name coq-lsp.lang)
+ (modules :standard \ utf_tests)
  (libraries uri coq-core.library))
+
+; We had to do this due to ppx_inline_test enabling backtraces
+
+(library
+ (name lang_tests)
+ (inline_tests)
+ (modules utf_tests)
+ (preprocess
+  (pps ppx_inline_test))
+ (libraries lang))