lean4-htt/src/Lean/Data/Lsp
2022-01-31 21:36:37 +01:00
..
Basic.lean fix: implement suggestions 2022-01-14 09:18:57 +01:00
Capabilities.lean feat: implement LSP workspace symbol request 2022-01-20 17:20:01 +01:00
Client.lean style: add copyright headers 2022-01-14 09:18:57 +01:00
Communication.lean chore: server: repr-print invalid header 2021-04-03 00:23:45 +02:00
Diagnostics.lean refactor: consistent naming of widget modules 2021-08-24 08:57:41 -07:00
Extra.lean feat: change error flag to progress kind in LeanFileProgressProcessingInfo 2021-12-15 13:00:05 +01:00
InitShutdown.lean feat: inform server if widgets are available 2022-01-29 10:04:25 +01:00
Internal.lean feat: implement partial ilean updates 2022-01-31 21:36:37 +01:00
Ipc.lean chore: fix servertest_init_exit 2022-01-14 09:18:57 +01:00
LanguageFeatures.lean feat: implement LSP workspace symbol request 2022-01-20 17:20:01 +01:00
TextSync.lean refactor: use Except instead of Option in the JSON code. 2021-06-07 12:10:10 +02:00
Utf16.lean fix: index out of bounds 2021-04-09 10:09:12 -07:00
Workspace.lean feat: register file watcher for .ilean files 2022-01-14 09:18:57 +01:00