diff --git a/src/emacs/lean-flycheck.el b/src/emacs/lean-flycheck.el
index dfaa314a3..960b8b66a 100644
--- a/src/emacs/lean-flycheck.el
+++ b/src/emacs/lean-flycheck.el
@@ -15,7 +15,7 @@
                          lean-flycheck-checker-options
                          '("--cache")
                          '(source-original)
-                         '((eval (lean-option-string)))
+                         '((eval (lean-option-string t)))
                          '("--")
                          '(source-inplace))))
     (when (string= system-type "windows-nt")
@@ -97,4 +97,27 @@
            (tempfiles (--map (concat tempfile it) exts)))
       (mapc #'flycheck-safe-delete tempfiles))))
 
+
+(defun lean-flycheck-error-list-buffer-width ()
+  "Return the width of flycheck-error list buffer"
+  (interactive)
+  (let* ((flycheck-error-window (get-buffer-window "*Flycheck errors*" t))
+         (window                (selected-window))
+         (body-width            (window-body-width window)))
+    (cond
+     ;; If "*Flycheck errors" buffer is available, use its width
+     (flycheck-error-window
+      (window-body-width flycheck-error-window))
+     ;; If lean-flycheck-msg-width is set, use it
+     (lean-flycheck-msg-width
+      lean-flycheck-msg-width)
+     ;; Can we split vertically?
+     ((window-splittable-p window nil)
+      body-width)
+     ;; Can we split horizontally?
+     ((window-splittable-p window t)
+      (/ body-width 2))
+     ;; In worst case, just use the same width of current window
+     (t body-width))))
+
 (provide 'lean-flycheck)
diff --git a/src/emacs/lean-option.el b/src/emacs/lean-option.el
index 3fd3ce85b..9e2cbc902 100644
--- a/src/emacs/lean-option.el
+++ b/src/emacs/lean-option.el
@@ -26,21 +26,30 @@
                  (-drop 1 str-list)))
     (string-join str-list "\n")))
 
-(defun lean-option-string ()
+(defun lean-option-string (&optional use-flycheck)
   "Return string of Lean options set by lean-set-option command"
-  (let ((pp-width-entry (assoc-string "pp.width" lean-global-option-alist)))
-    (unless pp-width-entry
-      (lean-update-option-alist "pp.width" lean-default-pp-width)))
-  (when lean-global-option-alist
-    (--reduce (format "%s %s" acc it)
-            (--map (format "-D%s=%s" (car it) (cdr it))
-                   lean-global-option-alist))))
+  (let* ((option-alist lean-global-option-alist)
+         (pp-width-entry (assoc-string "pp.width" option-alist)))
+    (cond (use-flycheck
+           (setq option-alist
+                 (lean-update-option-alist option-alist
+                                           "pp.width"
+                                           (lean-flycheck-error-list-buffer-width))))
+          ((not pp-width-entry)
+           (setq option-alist
+                 (lean-update-option-alist option-alist
+                                           "pp.width"
+                                           lean-default-pp-width))))
+    (when option-alist
+      (--reduce (format "%s %s" acc it)
+                (--map (format "-D%s=%s" (car it) (cdr it))
+                       option-alist)))))
 
-(defun lean-update-option-alist (name value)
-  (let ((needle (assoc-string name lean-global-option-alist)))
+(defun lean-update-option-alist (option-alist name value)
+  (let ((needle (assoc-string name 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))))
+      (setq option-alist (delq needle option-alist)))
+    (setq option-alist (cl-acons name value option-alist))))
 
 (defun lean-set-option-cont (option-record-alist)
   (let* ((key-list (-map 'car option-record-alist))
@@ -52,7 +61,10 @@
          (option-value (lean-option-read option)))
     (lean-server-send-cmd-async
      (lean-cmd-set option-name option-value)
-     (lambda (dummy) (lean-update-option-alist option-name option-value)))))
+     (lambda (dummy) (setq lean-global-option-alist
+                      (lean-update-option-alist lean-global-option-alist
+                                                option-name
+                                                option-value))))))
 
 (defun lean-set-option ()
   "Set Lean option."
diff --git a/src/emacs/lean-settings.el b/src/emacs/lean-settings.el
index 718585d30..9ae8f5100 100644
--- a/src/emacs/lean-settings.el
+++ b/src/emacs/lean-settings.el
@@ -68,12 +68,18 @@ show both of expressions and types.")
   "Maximum number of flycheck messages to displaylean-flychecker checker name
    (Restart required to be effective)"
   :group 'lean
-  :type 'int)
+  :type 'number)
 
 (defcustom lean-default-pp-width 120
   "Width of Lean error/warning messages"
   :group 'lean
-  :type 'int)
+  :type 'number)
+
+(defcustom lean-flycheck-msg-width nil
+  "Width of Lean error/warning messages"
+  :group 'lean
+  :type '(choice (const   :tag "Let lean-mode automatically detect this" nil)
+                 (integer :tag "Specify the value and force lean-mode to use")))
 
 (defcustom lean-flycheck-checker-options
   `("--flycheck"
diff --git a/src/emacs/test/lean-option-test.el b/src/emacs/test/lean-option-test.el
index 2c5950d0d..d9e2cd2ee 100644
--- a/src/emacs/test/lean-option-test.el
+++ b/src/emacs/test/lean-option-test.el
@@ -10,11 +10,13 @@
 (require 'lean-option)
 
 (ert-deftest lean-test-update-string-alist ()
-  (lean-update-option-alist "pp.implicit" 'true)
+  (setq lean-global-option-alist
+        (lean-update-option-alist lean-global-option-alist "pp.implicit" 'true))
   (should
    (equal (assoc-string "pp.implicit" lean-global-option-alist)
           '("pp.implicit" . true)))
-  (lean-update-option-alist "pp.implicit" 'false)
+  (setq lean-global-option-alist
+        (lean-update-option-alist lean-global-option-alist "pp.implicit" 'false))
   (should
    (equal (assoc-string "pp.implicit" lean-global-option-alist)
           '("pp.implicit" . false))))
@@ -25,7 +27,8 @@
                    (format "-D%s=%d"
                            "pp.width"
                            lean-default-pp-width)))
-  (lean-update-option-alist "pp.width" 80)
+  (setq lean-global-option-alist
+        (lean-update-option-alist lean-global-option-alist "pp.width" 80))
   (should (string= (lean-option-string)
                    (format "-D%s=%d"
                            "pp.width"