diff --git a/CHANGES.md b/CHANGES.md index 5f72d5c1c..94116f2b2 100644 --- a/CHANGES.md +++ b/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 diff --git a/controller/rq_completion.ml b/controller/rq_completion.ml index 1bbb4bbb6..10f2c7d75 100644 --- a/controller/rq_completion.ml +++ b/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); diff --git a/coq-lsp.opam b/coq-lsp.opam index 1a0f3831e..616cba804 100644 --- a/coq-lsp.opam +++ b/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 ] ] diff --git a/editor/code/CHANGELOG.md b/editor/code/CHANGELOG.md index cc368780d..2add29d1d 100644 --- a/editor/code/CHANGELOG.md +++ b/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 ---------------------- diff --git a/fleche/utf8.ml b/fleche/utf8.ml index 66313d75b..58c9ccbbb 100644 --- a/fleche/utf8.ml +++ b/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 =