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

feat(emacs/lean-server): show linja output in compilation mode

Browse source
This commit is contained in:
Gabriel Ebner 2016-10-13 12:11:19 -04:00 • committed by Leonardo de Moura
parent f969ed5d39
commit fd467584bd
1 changed files with 9 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -84,6 +84,14 @@
(proc (start-file-process
"linja" (format "*linja (%s)*" default-directory)
"linja")))
(set-process-sentinel proc (lambda (p e) (lean-server-restart))))))
(lexical-let ((buffer (current-buffer)))
(set-process-sentinel proc
(lambda (p e)
(with-current-buffer (process-buffer p) (compilation-mode))
(message "restarting lean")
(with-current-buffer buffer (lean-server-restart)))))
(temp-buffer-window-show (process-buffer proc))
(with-current-buffer (process-buffer proc)
(let ((buffer-read-only nil)) (erase-buffer))))))
(provide 'lean-server)