         (setq issue-level level)
         (setq message (substring message (length marker)))))
     (make-fstar-issue :level issue-level
-                      :filename filename
-                      :line-from (string-to-number line-from)
-                      :col-from (string-to-number col-from)
-                      :line-to (string-to-number line-to)
-                      :col-to (string-to-number col-to)
+                      :loc (make-fstar-location
+                            :filename filename
+                            :line-from (string-to-number line-from)
+                            :col-from (string-to-number col-from)
+                            :line-to (string-to-number line-to)
+                            :col-to (string-to-number col-to))
+                      :alternate-loc nil
                       :message message)))
+
+(defun fstar-subp-json--parse-location (json)
+  "Convert JSON info an fstar-mode location."
+  (let-alist json
+    (make-fstar-location
+     :filename .fname
+     :line-from (elt .beg 0)
+     :line-to (elt .end 0)
+     :col-from (elt .beg 1)
+     :col-to (elt .end 1))))
 
 (defun fstar-subp-json--parse-issue (json)
   "Convert JSON issue into fstar-mode issue."
   (let-alist json
     (make-fstar-issue :level (intern .level)
-                      :filename .range.fname
-                      :line-from (elt .range.beg 0)
-                      :line-to (elt .range.end 0)
-                      :col-from (elt .range.beg 1)
-                      :col-to (elt .range.end 1)
+                      :loc (fstar-subp-json--parse-location .range)
+                      :alternate-loc nil
                       :message .message)))
 
 (defun fstar-subp-parse-issues (response)

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