diff --git a/src/emacs/README.md b/src/emacs/README.md
index 07f601c249..8b9dff8300 100644
--- a/src/emacs/README.md
+++ b/src/emacs/README.md
@@ -20,9 +20,9 @@ Trying It Out
If things are working correctly, you should see the word ``Lean`` in the
Emacs mode line when you open a file with extension `.lean`. If you type
```lean
-check id
+#check id
```
-the word ``check`` will be underlined, and hovering over it will show
+the word ``#check`` will be underlined, and hovering over it will show
you the type of ``id``. The mode line will show ``FlyC:0/1``, indicating
that there are no errors and one piece of information displayed.
@@ -38,6 +38,7 @@ Key Bindings and Commands
| C-c SPC | run a command on the hole at point (`lean-hole`)
| C-c C-g | toggle showing current tactic proof goal (`lean-toggle-show-goal`) |
| C-c C-n | toggle showing next error in dedicated buffer (`lean-toggle-next-error`) |
+| C-c C-b | toggle showing output in inline boxes (`lean-message-boxes-toggle`) |
| C-c C-r | restart the lean server (`lean-server-restart`) |
| C-c ! n | flycheck: go to next error |
| C-c ! p | flycheck: go to previous error |
@@ -46,6 +47,17 @@ Key Bindings and Commands
In the default configuration, the Flycheck annotation `FlyC:n/n` indicates the
number of errors / responses from Lean; clicking on `FlyC` opens the Flycheck menu.
+
+Message Boxes
+================
+To view the output of commands such as `check` and `print` in boxes in the buffer, enable the feature using C-c C-b.
+If you then type
+```lean
+#check id
+```
+a box appears after the line showing the type of `id`. Customize `lean-message-boxes-enabled-captions` to choose categories of boxes.
+In particular, add `"trace output"` to the list to see proof states and other traces in the buffer.
+
Requirements
============
diff --git a/src/emacs/lean-message-boxes.el b/src/emacs/lean-message-boxes.el
new file mode 100644
index 0000000000..d53e59a92c
--- /dev/null
+++ b/src/emacs/lean-message-boxes.el
@@ -0,0 +1,108 @@
+;; -*- lexical-binding: t -*-
+;;
+;; Copyright (c) 2016 David Christiansen.
+;; Released under Apache 2.0 license as described in the file LICENSE.
+;;
+;; Author: David Christiansen
+;;
+;;; Code:
+
+(require 's)
+
+(defface lean-message-boxes-caption-face
+ '((t :inherit bold))
+ "Face for Lean message box captions."
+ :group 'lean)
+
+(defcustom lean-message-boxes-enabled-captions '("check result" "print result")
+ "Which captions should result in boxes?"
+ :group 'lean
+ :type '(repeat (choice (const "check result")
+ (const "print result")
+ (const "trace output"))))
+
+(defvar lean-message-boxes-enabledp nil
+ "Whether or not to display message boxes.")
+(make-variable-buffer-local 'lean-message-boxes-enabledp)
+
+(defun lean-message-boxes-toggle ()
+ "Toggle the display of message boxes."
+ (interactive)
+ (setq lean-message-boxes-enabledp (not lean-message-boxes-enabledp)))
+
+(defun lean-message-boxes-enable ()
+ "Enable the display of message boxes."
+ (interactive)
+ (setq lean-message-boxes-enabledp t))
+
+(defun lean-message-boxes-disable ()
+ "Disable the display of message boxes."
+ (interactive)
+ (setq lean-message-boxes-disabledp t))
+
+(defvar lean-message-boxes--overlays '()
+ "The overlays in the current buffer from Lean messages.")
+(make-variable-buffer-local 'lean-message-boxes--overlays)
+
+(defun lean-message-boxes--kill-overlays ()
+ "Delete all Lean message overlays in the current buffer."
+ (dolist (o lean-message-boxes--overlays)
+ (delete-overlay o))
+ (setq lean-message-boxes--overlays '()))
+
+(defun lean-message-boxes--pad-to (str width)
+ "Pad the string STR to a particular WIDTH."
+ (concat str (make-string (max 0 (- width (length str))) ?\ )))
+
+(defun lean-message-boxes-display (msgs)
+ "Show the messages MSGS in the Lean buffer as boxes when `lean-message-boxes-enabledp' is non-nil."
+ (lean-message-boxes--kill-overlays)
+ (when lean-message-boxes-enabledp
+ (dolist (msg msgs)
+ (let ((line (plist-get msg :pos_line))
+ (col (plist-get msg :pos_col))
+ (caption (plist-get msg :caption))
+ (text (plist-get msg :text)))
+ (when (member caption lean-message-boxes-enabled-captions)
+ (let ((overlay (lean-message-boxes--make-overlay line col caption text)))
+ (push overlay lean-message-boxes--overlays)))))))
+
+(defun lean-message-boxes--as-string (caption str)
+ "Construct a propertized string representing CAPTION and STR."
+ (let* ((caption-copy (concat caption))
+ (lines (s-lines str))
+ (w (apply #'max (mapcar #'length (cons caption lines))))
+ (top (concat "╭" (make-string (+ w 2) ?─) "╮"))
+ (horiz (concat "├" (make-string (+ w 2) ?─) "┤"))
+ (bot (concat "╰" (make-string (+ w 2) ?─) "╯")))
+ (put-text-property 0 (length caption-copy)
+ 'face 'lean-message-boxes-caption-face
+ caption-copy)
+ (apply #'concat
+ top "\n"
+ "│ " (lean-message-boxes--pad-to caption-copy w) " │\n"
+ horiz "\n"
+ (append
+ (mapcar
+ (lambda (l)
+ (concat "│ "
+ (lean-message-boxes--pad-to l w)
+ " │\n"))
+ lines)
+ (list bot)))))
+
+(defun lean-message-boxes--make-overlay (line col caption text)
+ "Construct a message box overlay at LINE and COL with CAPTION and TEXT."
+ (let* ((where (save-excursion (goto-char (point-min))
+ (forward-line (1- line))
+ (line-end-position)))
+ (overlay (make-overlay where (+ 1 where))))
+ (overlay-put overlay 'display
+ (concat "\n" (lean-message-boxes--as-string caption text) "\n"))
+ ;(overlay-put overlay 'face font-lock-builtin-face)
+ (overlay-put overlay 'mouse-face font-lock-warning-face)
+ (overlay-put overlay 'lean-is-output-overlay t)
+ overlay))
+
+(add-hook 'lean-server-show-message-hook 'lean-message-boxes-display)
+(provide 'lean-message-boxes)
diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index f212a9d8d4..dba7be614f 100644
--- a/src/emacs/lean-mode.el
+++ b/src/emacs/lean-mode.el
@@ -31,6 +31,7 @@
(require 'lean-info)
(require 'lean-hole)
(require 'lean-type)
+(require 'lean-message-boxes)
(defun lean-compile-string (exe-name args file-name)
"Concatenate exe-name, args, and file-name"
@@ -85,7 +86,7 @@
(local-set-key lean-keybinding-hole 'lean-hole)
(local-set-key lean-keybinding-lean-toggle-show-goal 'lean-toggle-show-goal)
(local-set-key lean-keybinding-lean-toggle-next-error 'lean-toggle-next-error)
- )
+ (local-set-key lean-keybinding-lean-message-boxes-toggle 'lean-message-boxes-toggle))
(define-abbrev-table 'lean-abbrev-table
'())
@@ -106,6 +107,7 @@
["Show type info" lean-show-type (and lean-eldoc-use eldoc-mode)]
["Toggle goal display" lean-toggle-show-goal t]
["Toggle next error display" lean-toggle-next-error t]
+ ["Toggle message boxes" lean-message-boxes-toggle t]
["Highlight pending tasks" lean-server-toggle-show-pending-tasks
:active t :style toggle :selected lean-server-show-pending-tasks]
["Find definition at point" lean-find-definition t]
diff --git a/src/emacs/lean-server.el b/src/emacs/lean-server.el
index 343fb6e960..a73731ff39 100644
--- a/src/emacs/lean-server.el
+++ b/src/emacs/lean-server.el
@@ -11,7 +11,7 @@
(require 'lean-pkg)
(require 'dash)
-(defcustom lean-server-show-message-hook '()
+(defcustom lean-server-show-message-hook '(lean-message-boxes-display)
"Hook run on messages from Lean, allowing custom display.
Each hook is a function that receives a list of message objects
@@ -22,7 +22,8 @@ least the following keys:
- :caption is a category of message, a string
- :text is the text to display, a string."
:group 'lean
- :type 'hook)
+ :type 'hook
+ :options '(lean-message-boxes-display))
(defstruct lean-server-session
path-file ; the leanpkg.path file of this lean server
diff --git a/src/emacs/lean-settings.el b/src/emacs/lean-settings.el
index 11ecfdad2d..fafc494318 100644
--- a/src/emacs/lean-settings.el
+++ b/src/emacs/lean-settings.el
@@ -129,4 +129,7 @@ false (nil)."
(defcustom lean-keybinding-lean-toggle-next-error (kbd "C-c C-n")
"Lean Keybinding for lean-toggle-next-error"
:group 'lean-keybinding :type 'key-sequence)
+(defcustom lean-keybinding-lean-message-boxes-toggle (kbd "C-c C-b")
+ "Lean Keybinding for lean-message-boxes-toggle"
+ :group 'lean-keybinding :type 'key-sequence)
(provide 'lean-settings)