 (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?
+    (cl-assert buffer-file-name)
+    (setf (fstar-issue-filename issue) buffer-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))


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

  (forward-char (min (- (point-at-eol) (point-at-bol)) column)))

(defun fstar--row-col-offset (line column)
  "Convert a (LINE, COLUMN) pair into a buffer offset."
  ;; LATER: This would be much easier if the interactive mode returned
  ;; an offset instead of a line an column.
  (save-excursion
    (fstar--goto line column)
    (point)))
