 ;;
 
 (require 'cl-lib)
+(require 'dash)
+(require 'dash-functional)
 (require 'lean-variable)
 (require 'lean-util)
 (require 'lean-cmd)
 (require 'lean-server)
 (require 'lean-debug)
+(require 'flymake)
 
-(defun lean-get-info-list (file-name line-number column)
-  "Get info list from lean server using file-name, line-number, and column.
-
-TODO(soonhok): for now, it ignores file-name and column."
-  (lean-server-send-cmd (lean-cmd-info line-number))
-  (while (not lean-global-info-processed)
-    (accept-process-output (lean-server-get-process) 0 50 t))
-  lean-global-info-list)
-
-(defun lean-filter-info-list (info-list when-pred)
-  "Filter info-list by given when-pred"
-  (cl-loop for info in info-list
-           when (funcall when-pred info)
-           collect info))
-
-(defun lean-bounds-of-thing-at-point ()
-  "Return the information of current symbol at point.
-
-The return valus has the form of '([symbol-string] [start-pos])"
-  (interactive)
-  (let ((bound (bounds-of-thing-at-point 'symbol))
-        start-pos end-pos sym)
-    (cond (bound
-           (setq start-pos (car bound))
-           (setq end-pos   (cdr bound))
-           (setq sym       (buffer-substring-no-properties start-pos end-pos)))
-          ((= (point) (point-max))
-           (setq start-pos (point))
-           (setq sym       ""))
-          (t
-           (setq start-pos (point))
-           (setq sym       (buffer-substring-no-properties start-pos (1+ start-pos)))))
-    (list sym start-pos)))
-
-(defun lean-eldoc-argument-list (string)
-  "Upcase and fontify STRING for use with `eldoc-mode'."
-  (propertize string 'face 'font-lock-variable-name-face))
-
-(defun lean-extract-info-at-pos (file-name line-number column start-pos)
-
-  (let*  ((info-list (lean-get-info-list file-name line-number column))
-          (info-list-at-pos (lean-filter-info-list
-                             info-list
-                             '(lambda (info) (and
-                                         (lean-info-column info)
-                                         (= start-column (lean-info-column info))))))
-          (typeinfo
-           (cl-first (lean-filter-info-list info-list-at-pos
-                                            'lean-typeinfo-p)))
-          (overload
-           (cl-first (lean-filter-info-list info-list-at-pos
-                                            'lean-overload-p)))
-          (synth
-           (cl-first (lean-filter-info-list info-list-at-pos
-                                            'lean-synth-p))))
-    (list typeinfo overload synth)))
-
-(defun lean-print-info (typeinfo overload synth sym-name)
-  "Given typeinfo, overload, and sym-name, print out information."
-  (when typeinfo
-    (let* ((overload-names  (lean-overload-names overload))
-           (overload-name   (cl-first overload-names))
-           (synth-value     (when synth (lean-synth-body-str synth)))
-           (name            (or synth-value overload-name sym-name))
-           (type-str        (lean-typeinfo-body-str typeinfo))
-           (type-output-str
-            (format "%s : %s"
-                    (propertize name 'face 'font-lock-variable-name-face)
-                    type-str))
-           (overload-output-str
-            (when overload-names
-              (format "\n%s with %s"
-                      (propertize "overloaded" 'face 'font-lock-keyword-face)
-                      (lean-string-join (cdr overload-names) ", "))))
-           (output-str (concat type-output-str overload-output-str)))
-      (message "%s" output-str))))
 
 (defun lean-fill-placeholder ()
   "Fill the placeholder with a synthesized expression by Lean."
   (interactive)
-  (let ((cur_char (buffer-substring-no-properties (point) (1+ (point)))))
-    (when (string= cur_char "_")
-      (let* ((file-name (buffer-file-name))
-             (line-number (line-number-at-pos))
-             (column (current-column))
-             (sym-info (lean-bounds-of-thing-at-point))
-             (sym-name (cl-first sym-info))
-             (start-pos (cl-second sym-info))
-             (start-column (- column (- (point) start-pos)))
-             typeinfo overload)
-        (cl-multiple-value-setq (typeinfo overload synth)
-          (lean-extract-info-at-pos file-name line-number column start-pos))
-        (when synth
-          (let ((synth-str
-                 (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)))))))
+  (let* ((info-record (lean-get-info-record-at-point))
+         (synth (and info-record (cl-first (lean-info-record-synth info-record)))))
+    (when synth
+      (let ((synth-str
+             (replace-regexp-in-string "?M_[0-9]+" "_" (lean-info-synth-body-str synth))))
+        (when (search " " synth-str)
+          (setq synth-str (concat "(" synth-str ")")))
+        (message "synth-str: %s" synth-str)
+        (delete-forward-char 1)
+        (insert synth-str)))))
 
 (defun lean-eldoc-documentation-function ()
   "Show information of lean expression at point if any"
   (interactive)
-  (let* ((file-name (buffer-file-name))
-         (line-number (line-number-at-pos))
-         (column (current-column))
-         (sym-info (lean-bounds-of-thing-at-point))
-         (sym-name (cl-first sym-info))
-         (start-pos (cl-second sym-info))
-         (start-column (- column (- (point) start-pos)))
-         typeinfo overload)
-    (cl-multiple-value-setq (typeinfo overload synth)
-      (lean-extract-info-at-pos file-name line-number column start-pos))
-    (lean-print-info typeinfo overload synth sym-name)))
+  (let ((info-record (lean-get-info-record-at-point))
+        info-string)
+    (cond
+     ((and info-record (lean-info-record-nay info-record))
+      (lean-server-log "NAY Detected")
+      (run-with-idle-timer lean-eldoc-nay-retry-time nil 'lean-eldoc-documentation-function))
+     (info-record
+      (setq info-string (lean-info-record-to-string info-record))
+      (when info-string
+        (message "%s" info-string))))))
+
+
+;; =======================================================
+;; Change Handling
+;; =======================================================
 
 (defun lean-before-change-function (beg end)
   "Function attached to before-change-functions hook.

 - lean-global-before-change-text            : text between beg and end

These information will be used by lean-after-changed-function."
  (setq lean-global-before-change-beg beg)
  (setq lean-global-before-change-end end)
  (setq lean-global-before-change-beg-line-number (line-number-at-pos beg))

           `(CHANGE-ONLY ,changed-lines))
          ;; Case "REMOVE"
          ((> old-lines-len new-lines-len)
           (setq removed-lines (-take (- old-lines-len new-lines-len) old-lines))
           ;; Make sure that we return it in reverse order
           (setq removed-lines (cl-sort removed-lines '>))
           (setq changed-lines new-lines)
           `(REMOVE ,removed-lines ,changed-lines))
          ;; Case "INSERT"
          ((< old-lines-len new-lines-len)
           (setq inserted-lines (-drop old-lines-len new-lines))
           ;; Make sure that we return it in sorted order
           (setq inserted-lines (cl-sort inserted-lines '<))
           (setq changed-lines old-lines)
