diff --git a/src/emacs/lean-cmd.el b/src/emacs/lean-cmd.el
index 7c86347e8..fe545c9d3 100644
--- a/src/emacs/lean-cmd.el
+++ b/src/emacs/lean-cmd.el
@@ -66,7 +66,7 @@ Lean produces a possible empty sequence of entries terminated with '--ENDINFO'"
 (defun lean-cmd-set (option-name option-value)
   "Set a Lean option [option-name] with [option-value].
 
-[option-name] must be a valid Lean option. Any option that can be
+ [option-name] must be a valid Lean option. Any option that can be
 set using the command set_option in a ‘.lean’ file is supported."
   `(SET ,option-name ,option-value))
 
@@ -100,6 +100,9 @@ It has the effect of evaluating a command in the end of the current file"
   "FINDG generates a sequence of declarations that may be used to “fill” a particular placeholder"
   `(FINDG ,line-number ,column-number ,patterns))
 
+(defun lean-cmd-wait ()
+  "Block server until all pending information has been computed."
+  `(WAIT))
 
 ;; Type
 ;; ====
@@ -265,16 +268,19 @@ It has the effect of evaluating a command in the end of the current file"
   "Convert valid command to string"
   (format "VALID"))
 (defun lean-cmd-findp-to-string (cmd)
-  "Convert valid command to string"
+  "Convert findp command to string"
   (format "FINDP %d\n%s"
           (lean-cmd-findp-get-line-number cmd)
           (lean-cmd-findp-get-prefix cmd)))
 (defun lean-cmd-findg-to-string (cmd)
-  "Convert valid command to string"
+  "Convert findg command to string"
   (format "FINDG %d %d\n%s"
           (lean-cmd-findg-get-line-number cmd)
           (lean-cmd-findg-get-column-number cmd)
           (lean-cmd-findg-get-patterns cmd)))
+(defun lean-cmd-wait-to-string (cmd)
+  "Convert wait command to string"
+  (format "WAIT"))
 
 (defun lean-cmd-to-string (cmd)
   "Convert command to string"
@@ -293,7 +299,8 @@ It has the effect of evaluating a command in the end of the current file"
     ('SHOW        (lean-cmd-show-to-string        cmd))
     ('VALID       (lean-cmd-valid-to-string       cmd))
     ('FINDP       (lean-cmd-findp-to-string       cmd))
-    ('FINDG       (lean-cmd-findg-to-string       cmd))))
+    ('FINDG       (lean-cmd-findg-to-string       cmd))
+    ('WAIT        (lean-cmd-wait-to-string        cmd))))
 
 ;; -- Test
 (cl-assert (string= (lean-cmd-to-string (lean-cmd-load "~/work/lean/basic.lean"))
@@ -316,6 +323,8 @@ It has the effect of evaluating a command in the end of the current file"
                     (concat "FINDP 42" "\n" "iff_")))
 (cl-assert (string= (lean-cmd-to-string (lean-cmd-findg 48 10 "+intro -and -elim"))
                     (concat "FINDG 48 10" "\n" "+intro -and -elim")))
+(cl-assert (string= (lean-cmd-to-string (lean-cmd-wait))
+                    (concat "WAIT")))
 
 ;; ----------------
 (provide 'lean-cmd)
diff --git a/src/emacs/lean-server.el b/src/emacs/lean-server.el
index 05c2e5fe5..a4d5afb7a 100644
--- a/src/emacs/lean-server.el
+++ b/src/emacs/lean-server.el
@@ -102,6 +102,8 @@
              ,(rx line-start (group "-- ENDFINDP") line-end))
     (FINDG   ,(rx line-start "-- BEGINFINDG" (* not-newline) line-end)
              ,(rx line-start (group "-- ENDFINDG") line-end))
+    (WAIT   ,(rx line-start "-- BEGINWAIT" line-end)
+             ,(rx line-start (group "-- ENDWAIT") line-end))
     (ERROR   ,(rx line-start "-- " (0+ not-newline) line-end)
              ,(rx line-start (group "-- ERROR" (0+ not-newline)) line-end)))
   "Regular expression pattern for lean-server message syntax")
@@ -258,6 +260,7 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd.
     ('VALID   (lean-server-check-current-file))
     ('FINDP   (lean-server-check-current-file))
     ('FINDG   (lean-server-check-current-file))))
+    ('WAIT    (lean-server-check-current-file))))
 
 (defun lean-server-after-send-cmd (cmd)
   "Operations to perform after sending a command."
@@ -276,6 +279,7 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd.
     ('VALID   ())
     ('FINDP   ())
     ('FINDG   ())))
+    ('WAIT    ())))
 
 (defun lean-server-send-cmd (cmd)
   "Send cmd to lean-server"