            `(CHANGE-ONLY ,changed-lines))
           ;; Case "REMOVE"
           ((> old-lines-len new-lines-len)
-           (setq removed-lines (lean-take-first-n old-lines (- 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 (lean-take-last-n new-lines (- new-lines-len old-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)

;;

(require 'cl-lib)
(require 'lean-variable)
(require 'lean-util)
(require 'lean-cmd)
(require 'lean-server)
(require 'lean-debug)

(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)))))))

(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)))

(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."
  (lean-server-get-process)
  (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))
