lean-mode.el

;;; lean-mode.el --- Minimal Lean 4 mode with eglot and infoview -*- lexical-binding: t; -*-

;;; Commentary:
;; Bare minimum Lean 4 support using eglot for LSP and a side window for infoview

;;; Code:

(require 'eglot)
(require 'jsonrpc)

(defvar lean-infoview-buffer "*Lean Infoview*")

(defconst lean-keywords
  '("import" "def" "theorem" "lemma" "example" "axiom" "inductive" "structure"
    "class" "instance" "variable" "universe" "namespace" "section" "end"
    "open" "export" "private" "protected" "mutual" "where" "let" "have"
    "show" "if" "then" "else" "match" "do" "return" "fun" "by" "calc"
    "extends" "deriving" "with" "without" "renaming" "hiding" "exposing"
    "abbrev" "opaque" "constant" "noncomputable"))

(defconst lean-types
  '("Prop" "Type" "Sort" "Nat" "Int" "String" "Char" "Bool" "List" "Array"
    "Option" "Sum" "Prod" "Unit" "Empty"))

(defconst lean-constants
  '("true" "false" "sorry"))

(defvar lean-font-lock-keywords
  `(("@\\[\\([^]]+\\)\\]" . font-lock-preprocessor-face)
    (,(regexp-opt lean-keywords 'symbols) . font-lock-keyword-face)
    (,(regexp-opt lean-types 'symbols) . font-lock-type-face)
    (,(regexp-opt lean-constants 'symbols) . font-lock-constant-face)
    ("\\<[A-Z][a-zA-Z0-9_]*\\>" . font-lock-type-face)
    ("\"[^\"]*\"" . font-lock-string-face)
    ("\\<[0-9]+\\>" . font-lock-constant-face)
    ("#\\w+" . font-lock-preprocessor-face)))

(defvar lean-mode-syntax-table
  (let ((table (make-syntax-table)))
    ;; Line comments: --
    (modify-syntax-entry ?- ". 12" table)
    (modify-syntax-entry ?\n ">" table)
    ;; Block comments: /- -/
    (modify-syntax-entry ?/ ". 14" table)
    table)
  "Syntax table for Lean mode.")

(define-derived-mode lean-mode prog-mode "Lean"
  "Simple mode for Lean 4 files."
  :syntax-table lean-mode-syntax-table
  (setq-local comment-start "-- ")
  (setq-local comment-end "")
  (setq-local comment-start-skip "--+\\s-*")
  (setq-local font-lock-defaults '(lean-font-lock-keywords)))

(add-to-list 'auto-mode-alist '("\\.lean\\'" . lean-mode))

(add-to-list 'eglot-server-programs
             '(lean-mode . ("lean" "--server")))

(defvar lean-infoview-mode-font-lock-keywords
  `(("^[0-9]+ goals?$" . font-lock-comment-face)
    ("^───+$" . font-lock-comment-face)
    ("^[^ \n][^\n]*:" . font-lock-function-name-face)
    ("⊢" . font-lock-keyword-face)
    (,(regexp-opt lean-keywords 'symbols) . font-lock-keyword-face))
  "Font lock keywords for Lean infoview.")

(define-derived-mode lean-infoview-mode special-mode "Lean-Info"
  "Mode for Lean infoview buffer."
  (setq-local font-lock-defaults '(lean-infoview-mode-font-lock-keywords))
  (setq-local word-wrap t)
  (setq-local truncate-lines nil)
  (font-lock-mode 1))

(defun lean--update-infoview (text)
  "Update infoview buffer with TEXT."
  (with-current-buffer (get-buffer-create lean-infoview-buffer)
    (unless (eq major-mode 'lean-infoview-mode)
      (lean-infoview-mode))
    (let ((inhibit-read-only t))
      (erase-buffer)
      (insert (or text "No goals"))
      (goto-char (point-min)))
    ;; Only display if window is already visible
    (when-let ((window (get-buffer-window (current-buffer))))
      (set-window-dedicated-p window nil))))

(defun lean--request-goal ()
  "Request plain goal at current position."
  (when-let ((server (eglot-current-server)))
    (jsonrpc-async-request
     server
     '$/lean/plainGoal
     (list :textDocument (eglot--TextDocumentIdentifier)
           :position (eglot--pos-to-lsp-position))
     :success-fn
     (lambda (result)
       (let* ((goals (plist-get result :goals))
              (num-goals (length goals)))
         (if (> num-goals 0)
             (let ((goal-text (mapconcat
                              (lambda (g) (format "%s" g))
                              goals
                              "\n\n───────────────────────────────\n\n")))
               (lean--update-infoview 
                (format "%d goal%s\n\n%s" 
                        num-goals 
                        (if (= num-goals 1) "" "s")
                        goal-text)))
           (lean--update-infoview "No goals"))))
     :error-fn (lambda (_err) nil)
     :timeout 0.5)))

(defun lean-toggle-infoview ()
  "Toggle the infoview window."
  (interactive)
  (if-let ((window (get-buffer-window lean-infoview-buffer)))
      (delete-window window)
    (when-let ((buf (get-buffer lean-infoview-buffer)))
      (display-buffer buf))))

(add-hook 'lean-mode-hook
          (lambda ()
            (eglot-ensure)
            (add-hook 'post-command-hook #'lean--request-goal nil t)))

(provide 'lean-mode)
;;; lean-mode.el ends here