Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
CHANGES: ------------------------------- - Update VSCode client dependencies, should bring some performance improvements to goal pretty printing (@ejgallego, ejgallego/coq-lsp#530) - Update goal display colors for light mode so they are actually readable now. (@bhaktishh, ejgallego/coq-lsp#539, fixes ejgallego/coq-lsp#532) - Added link to Python coq-lsp client by Pedro Carrot and Nuno Saavedra (@Nfsaavedra, ejgallego/coq-lsp#536) - Properly concatenate warnings from _CoqProject (@ejgallego, reported by @mituharu, ejgallego/coq-lsp#541, fixes ejgallego/coq-lsp#540) - Fix broken `coq/saveVo` and `coq/getDocument` requests due to a parsing problem with extra fields in their requests (@ejgallego, ejgallego/coq-lsp#547, reported by @Zimmi48) - `fcc` now understands the `--coqlib`, `--coqcorelib`, `--ocamlpath`, `-Q` and `-R` arguments (@ejgallego, ejgallego/coq-lsp#555) - Describe findlib status in `Workspace.describe`, which is printed in the output windows (@ejgallego, ejgallego/coq-lsp#556) - `coq-lsp` plugin loader will now be strict in case of a plugin failure, the previous loose behavior was more convenient for the early releases, but it doesn't make sense now and made things pretty hard to debug on the Windows installer (@ejgallego, ejgallego/coq-lsp#557) - Add pointers to Windows installers (@ejgallego, ejgallego/coq-lsp#559) - Recognize `Goal` and `Definition $id : ... .` as proof starters (@ejgallego, ejgallego/coq-lsp#561, reported by @Zimmi48, fixes ejgallego/coq-lsp#548) - Provide basic notation information on hover. This is intended for people to build their own more refined notation feedback systems (@ejgallego, ejgallego/coq-lsp#562) - Hover request can now be extended by plugins (@ejgallego, ejgallego/coq-lsp#562) - Updated LSP and JS client libs, notably to vscode-languageclient 9 (@ejgallego, ejgallego/coq-lsp#565) - Implement a LIFO document scheduler, this is heavier in the background as more documents will be checked, but provides a few usability improvements (@ejgallego, ejgallego/coq-lsp#566, fixes ejgallego/coq-lsp#563, reported by Ali Caglayan) - New lexical qed detection error recovery rule; this makes a very large usability difference in practice when editing inside proofs. (@ejgallego, ejgallego/coq-lsp#567, fixes ejgallego/coq-lsp#33) - `coq-lsp` is now supported by the `coq-nix-toolbox` (@Zimmi48, @CohenCyril, ejgallego/coq-lsp#572, via coq-community/coq-nix-toolbox#164 ) - Support for `-rifrom` in `_CoqProject` and in command line (`--rifrom`). Thanks to Lasse Blaauwbroek for the report. (@ejgallego, ejgallego/coq-lsp#581, fixes ejgallego/coq-lsp#579) - Export Query Goals API in VSCode client; this way other extensions can implement their own commands that query Coq goals (@amblafont, @ejgallego, ejgallego/coq-lsp#576, closes ejgallego/coq-lsp#558) - New `pretac` field for preprocessing of goals with a tactic using speculative execution, this is experimental for now (@amblafont, @ejgallego, ejgallego/coq-lsp#573, helps with ejgallego/coq-lsp#558) - Implement `textDocument/selectionRange` request, that will return the range of the Coq sentence underlying the cursor. In VSCode, this is triggered by the "Expand Selection" command. The implementation is partial: we only take into account the first position, and we only return a single range (Coq sentence) without parents. (@ejgallego, ejgallego/coq-lsp#582) - Be more robust to mixed-separator windows paths in workspace detection (@ejgallego, ejgallego/coq-lsp#583, fixes ejgallego/coq-lsp#569) - Adjust printing breaks in error and message panels (@ejgallego, @Alizter, ejgallego/coq-lsp#586, fixes ejgallego/coq-lsp#457 , fixes ejgallego/coq-lsp#458 , fixes ejgallego/coq-lsp#571)
- Loading branch information
