Merge branch 'v8.17' into v8.16

Author: ejgallego

CHANGES.md

@@ -28,8 +28,8 @@
  - Set Coq library name correctly (@ejgallego, #260)
  - `_CoqProject` file is now detected using LSP client `rootPath`
    (@ejgallego, #261)
- - Press `\` to trigger Unicode completion by the server. This
-   behavior is configurable, with "off", "regular", and extended
+ - You can press `\` to trigger Unicode completion by the server. This
+   behavior is configurable, with "off", "regular", and "extended"
    settings (@artagnon, @Alizter, ejgallego, #219).
 
 # coq-lsp 0.1.3: Event

controller/rq_completion.ml

@@ -62,12 +62,19 @@ let unicode_list point : Yojson.Safe.t list =
   (* Coq's CList.map is tail-recursive *)
   CList.map (mk_unicode_completion_item point) ulist
 
+let get_line_at_point ~(doc : Fleche.Doc.t) ~point =
+  (* Guard against bad line number *)
+  let line, _char = point in
+  let line = min line doc.contents.last.line in
+  let line = Array.get doc.contents.lines line in
+  if Fleche.Debug.completion then Lsp.Io.trace "completion" ("line: " ^ line);
+  line
+
 let get_char_at_point ~(doc : Fleche.Doc.t) ~point =
-  let line, char = point in
+  let _line, char = point in
   if char >= 1 then (
     let char = char - 1 in
-    let line = Array.get doc.contents.lines line in
-    if Fleche.Debug.completion then Lsp.Io.trace "completion" ("line: " ^ line);
+    let line = get_line_at_point ~doc ~point in
     let index = Fleche.Utf8.byte_of_char ~line ~char in
     if Fleche.Debug.completion then
       Lsp.Io.trace "completion" ("index: " ^ string_of_int index);

coq-lsp.opam

@@ -26,9 +26,8 @@ depends: [
   "yojson"       { >= "1.7.0" }
 
   # Uncomment this for releases
-  "coq"            {         >= "8.16.0" & < "8.17" }
-  "coq-serapi"     {         >= "8.16.0+0.16.2" & < "8.17" }
-  "camlp-streams"  {         >= "5.0"               }
+  "coq"          { >= "8.17" < "8.18" }
+  "coq-serapi"   { >= "8.17+rc1+0.17.1" < "8.18" }
 ]
 
 build: [ [ "dune" "build" "-p" name "-j" jobs ] ]

editor/code/CHANGELOG.md

@@ -3,9 +3,16 @@
 
 - The keybinding alt+enter in VSCode is now correctly scoped to be
   only active on Coq files.
-- Display an error message when VSCoq is detected to be active, as
-  they won't work well together.
+- Display an error message when the VSCoq extension is detected to be
+  active, as `coq-lsp` and VSCoq don't work well together.
+- Display an error message when the client and server versions don't
+  match.
 - [server-side] Support Unicode files
+- [server-side] Unicode completion on `\`, configurable in settings.
+- New infoview panel based on React.
+- New option in settings to enable Coq Debug mode (and backtraces)
+- Fixes a bug that made some `CoqProject` files not to be properly
+  detected.
 
 # coq-lsp 0.1.3: Event
 ----------------------

fleche/utf8.ml

@@ -45,9 +45,12 @@ let rec nth_aux s i n = if n = 0 then i else nth_aux s (next s i) (n - 1)
 let nth s n = nth_aux s 0 n
 
 (* end of camomille *)
+
+(* That's a tricky one, if the char we are requesting is out of bounds, then we
+   return the last index, 0 in the case line is empty. *)
 let byte_of_char ~line ~char =
   let ll = length line in
-  if ll <= char then ll else nth line char
+  if ll <= char then if ll = 0 then 0 else nth line ll - 1 else nth line char
 
 let find_char line byte =
   let rec f index n_chars =