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

fix(emacs): don't try to parse server stderr as json, instead notify on server crash

Browse source
This commit is contained in:
Sebastian Ullrich 2016-10-19 12:04:14 -04:00 • committed by Leonardo de Moura
parent 87f2f5397f
commit 133b70c0e3
2 changed files with 23 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -24,24 +24,35 @@
(setq lean-server-process nil (setq lean-server-process nil
lean-server-handler-tq nil))) lean-server-handler-tq nil)))
(defun lean-server-stderr-buffer-name ()
(format "*lean-server stderr (%s)*" (buffer-name)))
(defun lean-server-handle-signal (process event)
"Handle signals for lean-server-process"
(let ((event-string (s-trim event)))
(lean-debug "lean-server-handle-signal: %s"
(propertize event-string 'face '(:foreground "red")))
(if (s-contains? "abnormally" event)
(message "Lean server died. See buffer %s for details; use lean-server-restart to restart it"
(lean-server-stderr-buffer-name)))))
(defun lean-server-start () (defun lean-server-start ()
"Starts the lean server for the current buffer" "Starts the lean server for the current buffer"
(when (or (not lean-server-process) (when (or (not lean-server-process)
(not (equal (process-status lean-server-process) 'run))) (not (equal (process-status lean-server-process) 'run)))
(lean-server-stop) (lean-server-stop)
(setq lean-server-process (setq lean-server-process
(let* ((default-directory (or (lean-project-find-root) default-directory)) (let ((default-directory (or (lean-project-find-root) default-directory)))
; Setting process-connection-type is necessary, otherwise (make-process
; emacs truncates lines with >4096 bytes: :name "lean-server"
; https://debbugs.gnu.org/cgi/bugreport.cgi?bug=24531 :buffer (format "*lean-server (%s)*" (buffer-name))
(process-connection-type nil)) :command `(,(lean-get-executable lean-executable-name)
(start-file-process "lean-server" "--server"
(format "*lean-server (%s)*" (buffer-name)) ,(format "*%s*" (buffer-name)))
(lean-get-executable lean-executable-name) :coding 'utf-8
"--server" :noquery t
(format "*%s*" (buffer-name))))) :sentinel #'lean-server-handle-signal
(set-process-coding-system lean-server-process 'utf-8 'utf-8) :stderr (lean-server-stderr-buffer-name))))
(set-process-query-on-exit-flag lean-server-process nil)
(setq lean-server-handler-tq (tq-create lean-server-process)))) (setq lean-server-handler-tq (tq-create lean-server-process))))
(defun lean-server-restart () (defun lean-server-restart ()

1
src/library/trace.cpp
View file

@ -225,7 +225,6 @@ scope_traces_as_messages::scope_traces_as_messages(std::string const & stream_na
m_redirected_ios = std::unique_ptr<io_state>(new io_state(get_global_ios())); m_redirected_ios = std::unique_ptr<io_state>(new io_state(get_global_ios()));
m_buffer = std::make_shared<string_output_channel>(); m_buffer = std::make_shared<string_output_channel>();
m_redirected_ios->set_regular_channel(m_buffer); m_redirected_ios->set_regular_channel(m_buffer);
m_redirected_ios->set_diagnostic_channel(m_buffer);
m_scoped_ios = std::unique_ptr<scope_global_ios>(new scope_global_ios(*m_redirected_ios)); m_scoped_ios = std::unique_ptr<scope_global_ios>(new scope_global_ios(*m_redirected_ios));
} }
} }