diff --git a/src/emacs/lean-debug.el b/src/emacs/lean-debug.el index c5863821d6..753c24065e 100644 --- a/src/emacs/lean-debug.el +++ b/src/emacs/lean-debug.el @@ -5,7 +5,6 @@ ;; (require 'cl-lib) -(defvar lean-debug-mode nil) (defvar lean-debug-buffer-name "*lean-debug*") (defun lean-turn-on-debug-mode (&optional print-msg) @@ -47,4 +46,25 @@ (cons (propertize time-str 'face 'font-lock-keyword-face) args))))) +(defun lean-debug-mode-line-status-text () + "Get a text describing STATUS for use in the mode line." + (let ((text + ;; No Process : "X" + (cond ((not (lean-server-process-exist-p)) + "X") + ;; Number of Async Queue: *-n + ((> (lean-server-async-task-queue-len) 0) + (format "*-%d" (lean-server-async-task-queue-len))) + ;; Async Queue = 0 + (t "")))) + (concat " LeanDebug" text))) + +(define-minor-mode lean-debug-mode + "Minor mode for lean debugging." + + :init-value nil + :lighter lean-debug-mode-line + :group 'lean + :require 'lean) + (provide 'lean-debug) diff --git a/src/emacs/lean-settings.el b/src/emacs/lean-settings.el index 7d565bef83..718585d302 100644 --- a/src/emacs/lean-settings.el +++ b/src/emacs/lean-settings.el @@ -109,4 +109,10 @@ written." ;;(const :tag "Only Beyond lean-rule-column" lines-tail) )) +(defcustom lean-debug-mode-line '(:eval (lean-debug-mode-line-status-text)) + "Mode line lighter for Lean debug mode." + :group 'lean + :type 'sexp + :risky t) + (provide 'lean-settings)