| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | fix(leanls): move legacy_cmd -> options.non_lake_lsp_cmd | Julian Berman | 2022-02-18 | 1 | -4/+7 |
| | | |||||
| * | fix(leanls): support new src/lean directory | Gabriel Ebner | 2022-02-10 | 1 | -0/+6 |
| | | |||||
| * | fix(leanls): only use lake serve if lakefile.lean exists | Gabriel Ebner | 2022-02-09 | 1 | -15/+20 |
| | | |||||
| * | feat(leanls): start the LSP via lake serve (#1698) | Julian Berman | 2022-02-05 | 1 | -1/+18 |
| | | | | | | | | | | | Enables workspace symbols for the Lean 4 LSP. Older versions of Lake (and Lean 4) lack a serve command, so on those we fallback to the old behavior by directly starting the LSP. Closes: Julian/lean.nvim#229 Refs: leanprover/lake#46 | ||||
| * | feat(leanls): add root dir as command-line arg (#1634) | Gabriel Ebner | 2022-01-04 | 1 | -0/+4 |
| | | | | | | | | | | The argument is ignored by the server, but it is useful because it is shown by `htop`, `ps ax`, etc., so you can figure out which Lean servers are running. The lean3ls doesn't require a corresponding change: we use the `lean-language-server` wrapper, which appends the root directory itself to the wrapped `lean --server` command. | ||||
| * | fix: use forward delineated paths in leanlsps (#1610) | Julian Berman | 2021-12-26 | 1 | -1/+2 |
| | | |||||
| * | chore: clean up imports | Michael Lingelbach | 2021-11-25 | 1 | -1/+1 |
| | | |||||
| * | feat: expose configs | Michael Lingelbach | 2021-11-25 | 1 | -0/+41 |
 |
index : nvim-lspconfig | |
| [no description] | git mirrorbot |
| aboutsummaryrefslogtreecommitdiffstats |