max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(emacs): add tooltip to task overlays

Browse source
This commit is contained in:
Gabriel Ebner 2017-03-23 16:14:45 +01:00
parent af588add56
commit 24e19bdd00
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/emacs/lean-server.el
View file

@ -235,7 +235,8 @@
(let* ((reg (lean-server-task-region task))
(ov (make-overlay (car reg) (cdr reg))))
(setq lean-server-task-overlays (cons ov lean-server-task-overlays))
(overlay-put ov 'face 'lean-server-task-face)))))))
(overlay-put ov 'face 'lean-server-task-face)
(overlay-put ov 'help-echo (format "%s..." (plist-get task :desc)))))))))
(defun lean-server-toggle-show-pending-tasks ()
"Toggles highlighting of pending tasks"