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


(defun fstar-subp-cleanup-issue (issue &optional ov)
  "Fixup ISSUE: include a file name, and adjust line numbers wrt OV."
  (when (member (fstar-issue-filename issue) '("unknown" "<input>"))
    (cl-assert buffer-file-name)
    (setf (fstar-issue-filename issue) buffer-file-name))
  (unless (or (fstar--has-feature 'absolute-linums-in-errors) (null ov))
    (let ((linum (1- (line-number-at-pos (overlay-start ov)))))
      (setf (fstar-issue-line-from issue) (+ (fstar-issue-line-from issue) linum))
      (setf (fstar-issue-line-to issue) (+ (fstar-issue-line-to issue) linum))))
  issue)

(defun fstar-subp--in-issue-p (pt)
  "Check if PT is covered by an F* issue overlay."

  "Highlight ISSUE in current buffer.
PARENT is the overlay whose processing caused this issue to be
reported."
  (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)
