diff --git a/src/emacs/lean-option.el b/src/emacs/lean-option.el
index fdad3c82d..682a154f5 100644
--- a/src/emacs/lean-option.el
+++ b/src/emacs/lean-option.el
@@ -20,6 +20,17 @@
                  (-drop 1 str-list)))
     (string-join str-list "\n")))
 
+(defun lean-option-string ()
+  (--reduce (format "%s %s" acc it)
+            (--map (format "-D %s=%s" (car it) (cdr it))
+                   lean-global-option-alist)))
+
+(defun lean-update-option-alist (name value)
+  (let ((needle (assoc-string name lean-global-option-alist)))
+    (when needle
+      (setq lean-global-option-alist (delq needle lean-global-option-alist)))
+    (setq lean-global-option-alist (cl-acons name value lean-global-option-alist))))
+
 (defun lean-set-option-cont (option-record-alist)
   (let* ((key-list (-map 'car option-record-alist))
          (option-name
@@ -28,7 +39,9 @@
                            nil t "" nil (car key-list)))
          (option (cdr (assoc option-name option-record-alist)))
          (option-value (lean-option-read option)))
-    (lean-server-send-cmd-async (lean-cmd-set option-name option-value) 'message)))
+    (lean-server-send-cmd-async
+     (lean-cmd-set option-name option-value)
+     (lambda (dummy) (lean-update-option-alist option-name option-value)))))
 
 (defun lean-set-option ()
   "Set Lean option."
diff --git a/src/emacs/lean-server.el b/src/emacs/lean-server.el
index d6acb2965..6fa2d6e06 100644
--- a/src/emacs/lean-server.el
+++ b/src/emacs/lean-server.el
@@ -151,6 +151,7 @@
   (setq lean-global-server-last-time-sent nil)
   (setq lean-global-async-task-queue nil)
   (setq lean-global-nay-retry-counter 0)
+  (setq lean-global-option-alist nil)
   (lean-server-cancel-retry-timer))
 
 (defun lean-server-create-process ()
diff --git a/src/emacs/lean-variable.el b/src/emacs/lean-variable.el
index 5c3893672..7cb0a8aa9 100644
--- a/src/emacs/lean-variable.el
+++ b/src/emacs/lean-variable.el
@@ -54,4 +54,7 @@ where TYPE := INFO | SET | EVAL | OPTIONS | SHOW | FINDP | FINDG | ERROR,
 (defvar lean-global-before-change-text ""
   "Before-change text")
 
+(defvar lean-global-option-alist nil
+  "Current Lean options set by lean-set-option command")
+
 (provide 'lean-variable)