[new release] coq-lsp (0.1.6+8.16) #23390
Merged
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Language Server Protocol native server for Coq
CHANGES:
better highlighting and layout rendering (@artagnon, @ejgallego,
goals: lay foundation for pretty-printing goals (#96) ejgallego/coq-lsp#143, fixes [goal printing] Use jsCoq goal printing code ejgallego/coq-lsp#96)
fixes [proof/goals] Allow clients to specify Pp.t or string support. ejgallego/coq-lsp#321)
coq/getDocument
to get serialized full documentcontents. Thanks to Clément Pit-Claudel for feedback and ideas.
(@ejgallego, [completion] Trigger completion on quote char ejgallego/coq-lsp#350)
(@ejgallego, [code] Option to ignore .vo files automatically ejgallego/coq-lsp#365)
projects that contain several
_CoqProject
files in differentdirectories (@ejgallego, [lsp] [controller] Add support for workspace folders ejgallego/coq-lsp#374)
cc Add command to disable the language server ejgallego/coq-lsp#209)
exit
LSP notification(@artagnon, @ejgallego, [controller] Fix bug where the controller was not exiting ejgallego/coq-lsp#375, fixes Restarting LSP does not kill coq-lsp process ejgallego/coq-lsp#230)
coq-lsp.ok_diagnostics
setting (@artagnon, fleche, editor: strip Ok_diagnostic feature ejgallego/coq-lsp#129)(@ejallego, [nit] Scan also identifiers with doc, Coq's "qualids" ejgallego/coq-lsp#385)
vscode-languageclient
to 8.1.0 (@ejgallego, @Alizter,[code] Update to language-client 8.1.0 ejgallego/coq-lsp#383, fixes [code] [deps] Update to
vscode-languageclient
8.1.0 when it is released ejgallego/coq-lsp#273)number of total diagnostics, instead of only errors (@ejgallego,
[panel] Remove jquery in printing code ejgallego/coq-lsp#386)
the same name (@ejgallego, [hover] Fix precedence of hypothesis vs globals. ejgallego/coq-lsp#391, fixes [hover] Printing hypothesis prints the wrong type. ejgallego/coq-lsp#388)
trying to resume it if it didn't finish (@ejgallego, [scheduler] De-schedule document on didClose ejgallego/coq-lsp#392)
and containing a quote (') themselves (@ejgallego, [hover] Correctly handle identifiers before '.' and with ' ejgallego/coq-lsp#393)
[fleche] Add children info to the table-of-contents ejgallego/coq-lsp#395)
@Alizter, [code] Provide status bar button to stop / start the server. ejgallego/coq-lsp#378, closes Add command to disable the language server ejgallego/coq-lsp#209)
COQLIB
andCOQCORELIB
environment variables, added--coqcorelib
command line argument (@ejgallego, [coq] [workspace] [init] Recognize COQLIB and COQCORELIB ejgallego/coq-lsp#403)ocamlpath
from the command line (@ejgallego, [windows] Patches and instructions for windows install ejgallego/coq-lsp#408)(@ejgallego, reported by @Alizter, [client] Server status icon will now react properly to fatal server errors ejgallego/coq-lsp#411, fixes Status bar interacts badly when coq-lsp is not found ejgallego/coq-lsp#399)
coq-lsp.stats_on_hover_option
to re-enable it (@ejgallego, [hover] Info on memory and time is now disabled by default ejgallego/coq-lsp#412,fixes [config] Don't show perf data on hover by default. ejgallego/coq-lsp#398).
coq-lsp
can now save.vo
files for files opened in theeditor. Use the new "Save to .vo" command, or the new protocol
coq/saveVo
request (@ejgallego, [server] Add a command to save a .vo file. ejgallego/coq-lsp#417, fixes [commands] Add command to save .vo of current file ejgallego/coq-lsp#339)