From 133b70c0e34d04dee5efb3dca09b211b2e91db16 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 19 Oct 2016 12:04:14 -0400
Subject: [PATCH] fix(emacs): don't try to parse server stderr as json, instead
 notify on server crash

---
 src/emacs/lean-server.el | 35 +++++++++++++++++++++++------------
 src/library/trace.cpp    |  1 -
 2 files changed, 23 insertions(+), 13 deletions(-)

diff --git a/src/emacs/lean-server.el b/src/emacs/lean-server.el
index c55cc3a560..a0427ed803 100644
--- a/src/emacs/lean-server.el
+++ b/src/emacs/lean-server.el
@@ -24,24 +24,35 @@
     (setq lean-server-process 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 ()
   "Starts the lean server for the current buffer"
   (when (or (not lean-server-process)
             (not (equal (process-status lean-server-process) 'run)))
     (lean-server-stop)
     (setq lean-server-process
-          (let* ((default-directory (or (lean-project-find-root) default-directory))
-                 ; Setting process-connection-type is necessary, otherwise
-                 ; emacs truncates lines with >4096 bytes:
-                 ; https://debbugs.gnu.org/cgi/bugreport.cgi?bug=24531
-                 (process-connection-type nil))
-            (start-file-process "lean-server"
-                                (format "*lean-server (%s)*" (buffer-name))
-                                (lean-get-executable lean-executable-name)
-                                "--server"
-                                (format "*%s*" (buffer-name)))))
-    (set-process-coding-system lean-server-process 'utf-8 'utf-8)
-    (set-process-query-on-exit-flag lean-server-process nil)
+          (let ((default-directory (or (lean-project-find-root) default-directory)))
+            (make-process
+             :name "lean-server"
+             :buffer (format "*lean-server (%s)*" (buffer-name))
+             :command `(,(lean-get-executable lean-executable-name)
+                        "--server"
+                        ,(format "*%s*" (buffer-name)))
+             :coding 'utf-8
+             :noquery t
+             :sentinel #'lean-server-handle-signal
+             :stderr (lean-server-stderr-buffer-name))))
     (setq lean-server-handler-tq (tq-create lean-server-process))))
 
 (defun lean-server-restart ()
diff --git a/src/library/trace.cpp b/src/library/trace.cpp
index 2b7a4e1eae..6777843328 100644
--- a/src/library/trace.cpp
+++ b/src/library/trace.cpp
@@ -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_buffer = std::make_shared<string_output_channel>();
         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));
     }
 }