diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index ad3aaaf61..66089b643 100644
--- a/src/emacs/lean-mode.el
+++ b/src/emacs/lean-mode.el
@@ -107,7 +107,7 @@
     ["Execute lean"         lean-execute                      t]
     ["Create a new project" (call-interactively 'lean-project-create) (not (lean-project-inside-p))]
     "-----------------"
-    ["Show type info"       lean-eldoc-documentation-function lean-eldoc-use]
+    ["Show type info"       lean-show-type lean-eldoc-use]
     ["Fill a placeholder"   lean-fill-placeholder             (looking-at  (rx symbol-start "_"))]
     ["Find tag at point"    lean-find-tag                     t]
     ["Global tag search"    lean-global-search                t]
@@ -119,6 +119,9 @@
     ["Kill lean process"    lean-server-kill-process          t]
     ["Restart lean process" lean-server-restart-process       t]
     "-----------------"
+    ("Configuration"
+     ["Show type at point" lean-toggle-eldoc-mode :active t :style toggle :selected eldoc-mode])
+    "-----------------"
     ["Customize lean-mode" (customize-group 'lean)            t]))
 
 (defconst lean-hooks-alist
diff --git a/src/emacs/lean-type.el b/src/emacs/lean-type.el
index 607c3c859..c802be685 100644
--- a/src/emacs/lean-type.el
+++ b/src/emacs/lean-type.el
@@ -16,6 +16,13 @@
 (require 'lean-debug)
 (require 'flymake)
 
+(defun lean-toggle-eldoc-mode ()
+  "Toggle eldoc-mode"
+  (interactive)
+  (cond
+   (eldoc-mode (eldoc-mode -1))
+   (t          (eldoc-mode  1))))
+
 (defun lean-fill-placeholder-cont (info-record)
   "Continuation for lean-fill-placeholder"
   (let ((synth (and info-record (cl-first (lean-info-record-synth info-record)))))