 
 Take out \"BEGININFO\" and \"ENDINFO\" and Use \"ACK\" as a delim."
   (-split-on "-- ACK"
-             (--filter (not (or (string= "-- BEGININFO" it)
+             (--filter (not (or (string-prefix-p "-- BEGININFO" it)
                                 (string= "-- ENDINFO" it)))
                        (split-string str "\n"))))
 

                      (or (lean-info-type-parse string-seq)
                          (lean-info-overload-parse string-seq)
                          (lean-info-synth-parse string-seq)
                          (lean-info-identifier-parse string-seq)
                          (lean-info-symbol-parse string-seq)
                          (lean-info-nay-parse string-seq)))
             when result
             collect result)))


      (setq str (format "%s : %s"
                        (propertize name-str 'face 'font-lock-variable-name-face)
                        type-str)))
    (when (and str coercion-str)
      (setq str (format "%s (%s)"
                        (propertize coercion-str 'face 'font-lock-keyword-face)
                        str)))
    (when overload-str
      (setq str (concat str
                        (format "\n%s with %s"
                                (propertize "overloaded" 'face 'font-lock-keyword-face)
                                overload-str))))
    (when stale
      (setq str (format "[%s] %s"
                        (propertize "stale" 'face '(foreground-color . "red"))
                        str)))
    str))

(defun lean-get-info-record-at-point (cont)
  "Get info-record at the current point"
  (let ((file-name (buffer-file-name))
        (line-number (line-number-at-pos)))
    (lean-server-check-current-file file-name)
    (lean-server-send-cmd (lean-cmd-info line-number)
                          cont)))

(defun lean-get-full-name-at-point-cont (info-record)
  "Continuation of lean-get-full-name-at-point"
  (let ((id (cl-first (lean-info-record-identifier info-record))))
    (when id
      (lean-info-identifier-body-str id))))

(defun lean-get-full-name-at-point (cont)
  "Return the full-name at point (if any)"
  (lean-get-info-record-at-point
   (lambda (info-record)
     (funcall cont
              (lean-get-full-name-at-point-cont info-record)))))

(provide 'lean-info)
