     (fstar--goto line column)
     (point)))
 
-(defun fstar--match-strings-no-properties (ids str)
+(defun fstar--match-strings-no-properties (ids &optional str)
   "Get (match-string-no-properties ID STR) for each ID in IDS."
   (mapcar (lambda (num) (match-string-no-properties num str)) ids))
 


(defun fstar-subp-parse-issues (response)
  "Parse RESPONSE into a list of issues."
  (let ((start 0))
    (cl-loop while (string-match fstar-subp-issue-regexp response start)
             collect (fstar-subp-parse-issue response)
             do (setq start (match-end 0)))))

(defun fstar-subp-cleanup-issue (issue ov)
  "Fixup ISSUE: include a file name, and adjust line numbers wrt OV."
  (when (member (fstar-issue-filename issue) '("unknown" "<input>"))
    (setf (fstar-issue-filename issue) (buffer-file-name))) ;; FIXME ensure we have a file name?
  (unless fstar-compat--error-messages-use-absolute-linums
    (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))))

  "\\(.*?\\)(\\([[:digit:]]+\\),\\([[:digit:]]+\\)-\\([[:digit:]]+\\),\\([[:digit:]]+\\))")

(defconst fstar-subp-issue-regexp
  (concat "^" fstar-subp-issue-location-regexp "\\s-*:\\s-*"))

(defconst fstar-subp-also-see-regexp
  (concat "(Also see: " fstar-subp-issue-location-regexp ")"))

(defun fstar-subp-parse-issue (limit)
  "Construct an issue object from the current match data up to LIMIT."
  (pcase-let* ((issue-level 'error)
               (message (buffer-substring (match-end 0) limit))
               (`(,filename ,line-from ,col-from ,line-to ,col-to)
                (or (save-match-data
                      (when (string-match fstar-subp-also-see-regexp message)
                        (prog1 (fstar--match-strings-no-properties '(1 2 3 4 5) message)
                          (setq message (substring message 0 (match-beginning 0))))))
                    (fstar--match-strings-no-properties '(1 2 3 4 5)))))
    (pcase-dolist (`(,marker . ,level) '(("(Warning) " . warning)
                                         ("(Error) " . error)))
      (when (string-prefix-p marker message)
