feat(emacs): highlight flycheck and eldoc output

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))
 

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"

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)