From 6820c8bd9206de1887113548b5dbe044d29fe080 Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Wed, 12 Jan 2022 13:26:55 -0500 Subject: [PATCH] feat: create lsp workspaces automatically --- lean4-mode/lean4-mode.el | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/lean4-mode/lean4-mode.el b/lean4-mode/lean4-mode.el index 75ee8af98a..af9e30d344 100644 --- a/lean4-mode/lean4-mode.el +++ b/lean4-mode/lean4-mode.el @@ -172,7 +172,15 @@ enabled and disabled respectively.") ;; Flycheck (setq-local flycheck-disabled-checkers '()) ;; Lean massively benefits from semantic tokens, so change default to enabled - (setq-local lsp-semantic-tokens-enable t)) + (setq-local lsp-semantic-tokens-enable t) + (lean4-create-lsp-workspace)) + +(defun lean4-create-lsp-workspace () + "This will allow us to use emacs when a repo contains +multiple lean packages" + (when-let ((root (vc-find-root (buffer-file-name) + "lakefile.lean"))) + (lsp-workspace-folders-add root))) ;; Automode List ;;;###autoload