 (defconst fstar-subp--info-response-regex
   "^(defined at \\(.+?\\)(\\([0-9]+\\),\\([0-9]+\\)-\\([0-9]+\\),\\([0-9]+\\)))")
 
+(cl-defstruct fstar-pos-info
+  source-file def-start def-end type)
+
 (defun fstar-subp--info-continuation (continuation pos success response)
   "Handle the results (SUCCESS and RESPONSE) of an #info query at POS.
 If response is valid, forward results (only type information for

(defun fstar-subp-jump-to-issue (issue)
  "Jump to ISSUE in current buffer."
  (goto-char (fstar--row-col-offset (fstar-issue-line-from issue)
                               (fstar-issue-col-from issue))))

(defun fstar-subp--local-issue-p (issue)
  "Check if ISSUE came from the current buffer."

(defun fstar-subp-highlight-issue (issue)
  "Highlight ISSUE in current buffer."
  (let* ((from (fstar--row-col-offset (fstar-issue-line-from issue)
                                      (fstar-issue-col-from issue)))
         (to (fstar--row-col-offset (fstar-issue-line-to issue)
                                    (fstar-issue-col-to issue)))
         (overlay (make-overlay from (max to (1+ from)) (current-buffer) t nil)))
    (overlay-put overlay 'fstar-subp-issue t)
    (overlay-put overlay 'face (fstar-subp-issue-face issue))
