feat(emacs/lean-debug): add lean-debug minor-mode

close #177
This commit is contained in:
Soonho Kong 2014-09-15 16:40:11 -07:00
parent 851444b77a
commit aa9fe958a9
2 changed files with 27 additions and 1 deletions

View file

@ -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)

View file

@ -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)