   "Highlight ISSUE in current buffer.
 PARENT is the overlay whose processing caused this issue to be
 reported."
-  (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)))
+  (let* ((loc (fstar-issue-loc issue))
+         (from (fstar--row-col-offset (fstar-location-line-from loc)
+                                 (fstar-location-col-from loc)))
+         (to (fstar--row-col-offset (fstar-location-line-to loc)
+                               (fstar-location-col-to loc)))
          (overlay (make-overlay from (max to (1+ from)) (current-buffer) t nil)))
     (overlay-put overlay 'fstar-subp-issue t)
     (overlay-put overlay 'fstar-subp-issue-parent-overlay parent)

      (unless (fstar--has-feature 'json-subp)
        (fstar-subp--pop)))))

(cl-defstruct fstar-issue
  level filename line-from line-to col-from col-to message)

(defconst fstar-subp-issue-location-regexp
  "\\(.*?\\)(\\([[:digit:]]+\\),\\([[:digit:]]+\\)-\\([[:digit:]]+\\),\\([[:digit:]]+\\))")


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

(defun fstar-subp--local-issue-p (issue)
  "Check if ISSUE came from the current buffer."
  (string= (expand-file-name buffer-file-name)
           (expand-file-name (fstar-location-filename (fstar-issue-loc issue)))))

(defun fstar-subp-parse-and-highlight-issues (status response overlay)
  "Parse issues in RESPONSE (caused by processing OVERLAY) and display them.
