feat(emacs): Add the display of Lean messages in transient boxes

Informational output is usually seen in Flycheck in lean-mode. Now, it
can also be displayed in transient boxes that are not really part of
the buffer. This allows them to be quickly visually compared.

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
 | <kbd>C-c SPC</kbd> | run a command on the hole at point (`lean-hole`)
 | <kbd>C-c C-g</kbd> | toggle showing current tactic proof goal (`lean-toggle-show-goal`)              |
 | <kbd>C-c C-n</kbd> | toggle showing next error in dedicated buffer (`lean-toggle-next-error`)        |
+| <kbd>C-c C-b</kbd> | toggle showing output in inline boxes (`lean-message-boxes-toggle`)             |
 | <kbd>C-c C-r</kbd> | restart the lean server (`lean-server-restart`)                                 |
 | <kbd>C-c ! n</kbd> | flycheck: go to next error                                                      |
 | <kbd>C-c ! p</kbd> | 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 <kbd>C-c C-b</kbd>.
+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
 ============
 

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)

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]

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

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)