Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
CHANGES: --------------------- - The info / goal view now uses jsCoq's client-side rendering, with better highlighting and layout rendering (@artagnon, @ejgallego, ejgallego/coq-lsp#143, fixes ejgallego/coq-lsp#96) - Printing method is now configurable by the user (@ejgallego, ejgallego/coq-lsp#143, fixes ejgallego/coq-lsp#321) - Trigger completion on quote char "'" (@ejgallego, ejgallego/coq-lsp#350) - Fix typo on keybinding config for show goals (@tomtomjhj, ejgallego/coq-lsp#357) - New request `coq/getDocument` to get serialized full document contents. Thanks to Clément Pit-Claudel for feedback and ideas. (@ejgallego, ejgallego/coq-lsp#350) - Auto-ignore Coq object files; can be disabled in config (@ejgallego, ejgallego/coq-lsp#365) - Support workspaces with multiple roots, this is very useful for projects that contain several `_CoqProject` files in different directories (@ejgallego, ejgallego/coq-lsp#374) - Add VS Code commands to start / stop the server (@ejgallego, ejgallego/coq-lsp#377, cc ejgallego/coq-lsp#209) - Fix bug that made the server not exit on `exit` LSP notification (@artagnon, @ejgallego, ejgallego/coq-lsp#375, fixes ejgallego/coq-lsp#230) - Lay the foundation for server tests (@artagnon, ejgallego/coq-lsp#356) - Remove the `coq-lsp.ok_diagnostics` setting (@artagnon, ejgallego/coq-lsp#129) - Print abbreviations on hover (@ejgallego, ejgallego/coq-lsp#384) - Print hover types without parenthesis (@ejgallego, ejgallego/coq-lsp#384) - Parse identifiers with dot for hover and jump to definition (@ejallego, ejgallego/coq-lsp#385) - Update `vscode-languageclient` to 8.1.0 (@ejgallego, @Alizter, ejgallego/coq-lsp#383, fixes ejgallego/coq-lsp#273) - Fix typo on max_errors checking, this made coq-lsp stop on the number of total diagnostics, instead of only errors (@ejgallego, ejgallego/coq-lsp#386) - Hover symbol information: hypothesis names must shadow globals of the same name (@ejgallego, ejgallego/coq-lsp#391, fixes ejgallego/coq-lsp#388) - De-schedule document on didClose, otherwise the scheduler will keep trying to resume it if it didn't finish (@ejgallego, ejgallego/coq-lsp#392) - Hover symbol information: correctly handle identifiers before '.' and containing a quote (') themselves (@ejgallego, ejgallego/coq-lsp#393) - Add children entries to the table-of-contents (@ejgallego, ejgallego/coq-lsp#394) - Invalidate Coq's imperative cache on error (@ejgallego, @r-muhairi, ejgallego/coq-lsp#395) - Add status bar button to toggle server run status (@ejgallego, @Alizter, ejgallego/coq-lsp#378, closes ejgallego/coq-lsp#209) - Support for `COQLIB` and `COQCORELIB` environment variables, added `--coqcorelib` command line argument (@ejgallego, ejgallego/coq-lsp#403) - Protocol infrastructure for code lenses (@ejgallego, ejgallego/coq-lsp#396) - Set binary more for protocol input / output (@ejgallego, ejgallego/coq-lsp#408) - Allow to set `ocamlpath` from the command line (@ejgallego, ejgallego/coq-lsp#408) - Windows support (@ejgallego, @jim-portegies, ejgallego/coq-lsp#408) - Scroll active goal into view (@ejgallego, ejgallego/coq-lsp#410, fixes ejgallego/coq-lsp#381) - Server status icon will now react properly to fatal server errors (@ejgallego, reported by @Alizter, ejgallego/coq-lsp#411, fixes ejgallego/coq-lsp#399) - Info on memory and time is now disabled by default, new option `coq-lsp.stats_on_hover_option` to re-enable it (@ejgallego, ejgallego/coq-lsp#412, fixes ejgallego/coq-lsp#398). - `coq-lsp` can now save `.vo` files for files opened in the editor. Use the new "Save to .vo" command, or the new protocol `coq/saveVo` request (@ejgallego, ejgallego/coq-lsp#417, fixes ejgallego/coq-lsp#339)
- Loading branch information