 
 (defun fstar-indentation-points ()
   "Find reasonable indentation points on the current line."
-  (let ((points)) ;; FIXME first line?
+  (let ((points))
     (save-excursion
-      (forward-line -1)
-      (while (re-search-forward "\\s-+" (point-at-eol) t)
-        (push (current-column) points)))
+      (when (= (forward-line -1) 0) ;; Recognize the first line
+        (while (re-search-forward "\\s-+" (point-at-eol) t)
+          (push (current-column) points))))
     (when points
       (let ((mn (apply #'min points)))
         (push (+ 2 mn) points)

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

then returns nil (in that case, results are displayed
asynchronously after the fact)."
  (-if-let* ((hole-info (get-text-property (point) 'fstar--match-var-type)))
      (format "This hole has type `%s'" (car hole-info))
    (when (and (fstar--has-feature 'info) (fstar-subp-available-p)
               (not (fstar-subp--in-issue-p (point))))
