From d54c4e11c2d5e3932c5678b07f41ff4c554da136 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 18 Sep 2017 17:09:33 +0200 Subject: [PATCH] feat(emacs): highlight flycheck and eldoc output --- src/emacs/lean-flycheck.el | 2 +- src/emacs/lean-info.el | 8 ++++++++ src/emacs/lean-type.el | 2 +- 3 files changed, 10 insertions(+), 2 deletions(-) diff --git a/src/emacs/lean-flycheck.el b/src/emacs/lean-flycheck.el index 4b17350bea..e0b6488051 100644 --- a/src/emacs/lean-flycheck.el +++ b/src/emacs/lean-flycheck.el @@ -57,7 +57,7 @@ ("warning" 'warning) ("information" 'info) (_ 'info)) - text + (lean-highlight-string text) :filename file_name :checker checker :buffer buffer)) diff --git a/src/emacs/lean-info.el b/src/emacs/lean-info.el index 09b3ca292f..6eb96d4f2f 100644 --- a/src/emacs/lean-info.el +++ b/src/emacs/lean-info.el @@ -56,6 +56,14 @@ ;; current window of current buffer is selected (i.e., in focus) (eq (current-buffer) (window-buffer)))) +(defun lean-highlight-string (str) + "Returns 'str' highlighted in lean-info-mode" + (lean-ensure-info-buffer " Lean tmp buffer") + (lean-with-info-output-to-buffer (get-buffer " Lean tmp buffer") + (princ str) + (font-lock-fontify-buffer) + (buffer-string))) + (defun lean-get-info-record-at-point (cont) "Get info-record at the current point" (with-demoted-errors "lean get info: %s" diff --git a/src/emacs/lean-type.el b/src/emacs/lean-type.el index ab49116278..ad77700d04 100644 --- a/src/emacs/lean-type.el +++ b/src/emacs/lean-type.el @@ -55,7 +55,7 @@ (propertize expr 'face 'font-lock-variable-name-face) type)))) (when type - (setq type-str type)) + (setq type-str (lean-highlight-string type))) (when tactic_params (setq tactic_params (-map-indexed (lambda (i param) (if (eq i tactic_param_idx)