From 1227e01dd26d88d135e0cff37dfdd546f2a01f6f Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Sat, 29 Oct 2016 12:06:11 -0400
Subject: [PATCH] fix(emacs): faster lean-info updates

---
 src/emacs/lean-flycheck.el |  1 +
 src/emacs/lean-info.el     | 44 ++++++++++++++++++++++++++++++++++++++
 src/emacs/lean-mode.el     | 23 ++------------------
 3 files changed, 47 insertions(+), 21 deletions(-)
 create mode 100644 src/emacs/lean-info.el

diff --git a/src/emacs/lean-flycheck.el b/src/emacs/lean-flycheck.el
index 3a368f38aa..c7c31d1eb2 100644
--- a/src/emacs/lean-flycheck.el
+++ b/src/emacs/lean-flycheck.el
@@ -8,6 +8,7 @@
 (require 'flycheck)
 (require 'lean-settings)
 (require 'lean-server)
+(require 'lean-info)
 
 (defun lean-toggle-flycheck-mode ()
   "Toggle flycheck-mode"
diff --git a/src/emacs/lean-info.el b/src/emacs/lean-info.el
new file mode 100644
index 0000000000..96d7149731
--- /dev/null
+++ b/src/emacs/lean-info.el
@@ -0,0 +1,44 @@
+;; -*- lexical-binding: t -*-
+;;
+;;; lean-info.el --- Emacs mode for Lean theorem prover
+;;
+;; Copyright (c) 2016 Gabriel Ebner. All rights reserved.
+;;
+;; Author: Gabriel Ebner <gebner@gebner.org>
+;; Maintainer: Gabriel Ebner <gebner@gebner.org>
+;; Created: Oct 29, 2016
+;; Keywords: languages
+;; Version: 0.1
+;; URL: https://github.com/leanprover/lean/blob/master/src/emacs
+;;
+;; Released under Apache 2.0 license as described in the file LICENSE.
+;;
+
+;; Lean Info Mode (for "*lean-info*" buffer)
+;; Automode List
+;;;###autoload
+(define-derived-mode lean-info-mode prog-mode "Lean-Info"
+  "Major mode for Lean Info Buffer"
+  :syntax-table lean-syntax-table
+  :group 'lean
+  (set (make-local-variable 'font-lock-defaults) lean-info-font-lock-defaults)
+  (set (make-local-variable 'indent-tabs-mode) nil)
+  (set 'compilation-mode-font-lock-keywords '())
+  (set-input-method "Lean")
+  (set (make-local-variable 'lisp-indent-function)
+       'common-lisp-indent-function))
+
+(defconst lean-info-buffer-name "*lean-info*")
+
+(defmacro with-output-to-lean-info (&rest body)
+  `(let ((lean-info-buffer (get-buffer lean-info-buffer-name)))
+     (if (and lean-info-buffer (get-buffer-window lean-info-buffer))
+         (with-current-buffer lean-info-buffer
+           (setq buffer-read-only nil)
+           (erase-buffer)
+           (setq standard-output lean-info-buffer)
+           . ,body)
+       (let ((temp-buffer-setup-hook #'lean-info-mode))
+         (with-output-to-temp-buffer lean-info-buffer-name . ,body)))))
+
+(provide 'lean-info)
diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index a5f6172444..083ff2e5bc 100644
--- a/src/emacs/lean-mode.el
+++ b/src/emacs/lean-mode.el
@@ -21,12 +21,13 @@
 (require 'eri)
 (require 'lean-util)
 (require 'lean-settings)
-(require 'lean-flycheck)
 (require 'lean-input)
 (require 'lean-syntax)
 (require 'lean-project)
 (require 'lean-company)
 (require 'lean-server)
+(require 'lean-flycheck)
+(require 'lean-info)
 
 (defun lean-compile-string (exe-name args file-name)
   "Concatenate exe-name, args, and file-name"
@@ -50,12 +51,6 @@
               (or arg "")
               (shell-quote-argument (f-full target-file-name))))))
 
-(defconst lean-info-buffer-name "*lean-info*")
-
-(defmacro with-output-to-lean-info (&rest body)
-  `(let* ((temp-buffer-setup-hook #'lean-info-mode))
-     (with-output-to-temp-buffer lean-info-buffer-name . ,body)))
-
 (defun lean-show-goal-at-pos ()
   "Show goal at the current point."
   (interactive)
@@ -238,19 +233,5 @@ Invokes `lean-mode-hook'.
   (eval-after-load 'flycheck
     '(lean-flycheck-init)))
 
-;; Lean Info Mode (for "*lean-info*" buffer)
-;; Automode List
-;;;###autoload
-(define-derived-mode lean-info-mode prog-mode "Lean-Info"
-  "Major mode for Lean Info Buffer"
-  :syntax-table lean-syntax-table
-  :group 'lean
-  (set (make-local-variable 'font-lock-defaults) lean-info-font-lock-defaults)
-  (set (make-local-variable 'indent-tabs-mode) nil)
-  (set 'compilation-mode-font-lock-keywords '())
-  (set-input-method "Lean")
-  (set (make-local-variable 'lisp-indent-function)
-       'common-lisp-indent-function))
-
 (provide 'lean-mode)
 ;;; lean-mode.el ends here