 
 (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

      (make-fstar-issue
       :level (intern .level)
       :locs (append (mapcar #'fstar-subp-json--parse-location .ranges) alt-locs)
       :message (fstar--string-trim msg)))))

(defun fstar-subp-parse-issues (response)
  "Parse RESPONSE into a list of issues."

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

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