michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(emacs): replace metavar '?M_n' with '_' in synthed expr

Browse source
This commit is contained in:
Soonho Kong 2014-08-14 17:59:28 -07:00
parent 2edb53397f
commit b18124e1a2
1 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/emacs/lean-type.el
View file

@ -102,8 +102,12 @@ The return valus has the form of '([symbol-string] [start-pos])"
(cl-multiple-value-setq (typeinfo overload synth) (cl-multiple-value-setq (typeinfo overload synth)
(lean-extract-info-at-pos file-name line-number column start-pos)) (lean-extract-info-at-pos file-name line-number column start-pos))
(when synth (when synth
(delete-forward-char 1) (let ((synth-str
(insert (concat "(" (lean-synth-body-str synth) ")"))))))) (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 () (defun lean-eldoc-documentation-function ()
"Show information of lean expression at point if any" "Show information of lean expression at point if any"