Don't use child directories of "lake-packages" as workspace roots

leanprover-community · Aug 10, 2023 · fde364e · fde364e
1 parent d1c9364
commit fde364e
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/lean4-mode.el b/lean4-mode.el
@@ -190,6 +190,9 @@ This will allow us to use Emacs when a repo contains multiple lean packages."
   (when-let ((file-name (buffer-file-name))
              (root (vc-find-root (buffer-file-name)
                                  "lakefile.lean")))
+    (while (let ((parent (f-parent root)))
+             (when (string= (f-filename parent) "lake-packages")
+               (setq root (f-parent parent)))))
     (lsp-workspace-folders-add root)))
 
 ;; Automode List