 (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:]]+\\))")
+
 (defconst fstar-subp-issue-regexp
-  "\\(.*?\\)(\\([[:digit:]]+\\),\\([[:digit:]]+\\)-\\([[:digit:]]+\\),\\([[:digit:]]+\\))\\s-*:\\s-*\\(.*\\)")
+  (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 (context)
   "Construct an issue object from the current match data and CONTEXT."
-  (pcase-let ((issue-level 'error)
-              (`(,filename ,line-from ,col-from ,line-to ,col-to ,message)
-               (mapcar (lambda (num) (match-string-no-properties num context))
-                       '(1 2 3 4 5 6))))
-    (let ((warning-marker "(Warning) "))
-      (when (string-prefix-p warning-marker message)
-        (setq issue-level 'warning)
-        (setq message (substring message (length warning-marker)))))
+  (pcase-let* ((issue-level 'error)
+               (message (match-string-no-properties 6 context))
+               (`(,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) context))))
+    (pcase-dolist (`(,marker . ,level) '(("(Warning) " . warning)
+                                         ("(Error) " . error)))
+      (when (string-prefix-p marker message)
+        (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)

    (fstar--goto line column)
    (point)))

;;;; Overlay classification

(defun fstar-subp-issue-overlay-p (overlay)

nil and the corresponding continuation calls `eldoc-message'."
  (when (and fstar-compat--can-use-info (fstar-subp-available-p))
    (fstar-subp--query (fstar-subp--info-query (point))
                       (apply-partially #'fstar-subp--info-continuation
                                        #'fstar--eldoc-continuation
                                        (point)))
    ;; FIXME: use pos-tip for errors, or show errors in eldoc
    nil))

