 
 (defun fstar-issue-message-with-level (issue)
   "Concatenate ISSUE's level and message."
-  (format "(%s) %s"
+  (format "(%s%s) %s"
           (capitalize (symbol-name (fstar-issue-level issue)))
+          (let ((numopt (fstar-issue-number issue)))
+            (if numopt
+                (concat " " (number-to-string numopt))
+                ""))
           (fstar-issue-message issue)))
 
 (defconst fstar-subp-issue-location-regexp

                                :col-from (string-to-number col-from)
                                :line-to (string-to-number line-to)
                                :col-to (string-to-number col-to)))
                      :message message)))

(defun fstar-subp-json--extract-alt-locs (message)
  "Extract secondary locations (see also, Also see) from MESSAGE.

  (run-hook-with-args 'fstar-subp-overlay-processed-hook overlay status response))

(cl-defstruct fstar-issue
  level locs message number)

(defun fstar-issue-alt-locs (issue)
  "Extract locations attached to ISSUE, except the first one."
