From b18124e1a2428fcd3c0704991a5e5eb8864b9bd2 Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Thu, 14 Aug 2014 17:59:28 -0700
Subject: [PATCH] feat(emacs): replace metavar '?M_n' with '_' in synthed expr

---
 src/emacs/lean-type.el | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/emacs/lean-type.el b/src/emacs/lean-type.el
index f681f72b3..bcee9294b 100644
--- a/src/emacs/lean-type.el
+++ b/src/emacs/lean-type.el
@@ -102,8 +102,12 @@ The return valus has the form of '([symbol-string] [start-pos])"
         (cl-multiple-value-setq (typeinfo overload synth)
           (lean-extract-info-at-pos file-name line-number column start-pos))
         (when synth
-          (delete-forward-char 1)
-          (insert (concat "(" (lean-synth-body-str synth) ")")))))))
+          (let ((synth-str
+                 (replace-regexp-in-string "?M_[0-9]+" "_" (lean-synth-body-str synth))))
+            (when (search " " synth-str)
+              (setq synth-str (concat "(" synth-str ")")))
+            (delete-forward-char 1)
+            (insert synth-str)))))))
 
 (defun lean-eldoc-documentation-function ()
   "Show information of lean expression at point if any"