 (defun fstar-subp-highlight-issue (issue)
   "Highlight ISSUE in current buffer."
   (let* ((from (fstar-issue-offset (fstar-issue-line-from issue)
-                              (fstar-issue-col-from issue)))
+                                   (fstar-issue-col-from issue)))
          (to (fstar-issue-offset (fstar-issue-line-to issue)
-                            (fstar-issue-col-to issue)))
+                                 (fstar-issue-col-to issue)))
          (overlay (make-overlay from (max to (1+ from)) (current-buffer) t nil)))
     (overlay-put overlay 'fstar-subp-issue t)
     (overlay-put overlay 'face (fstar-subp-issue-face issue))

(defun fstar-subp-jump-to-issue (issue)
  "Jump to ISSUE in current buffer."
  (goto-char (fstar-issue-offset (fstar-issue-line-from issue)
                            (fstar-issue-col-from issue))))

(defun fstar-subp--local-issue-p (issue)
  "Check if ISSUE came from the current buffer."

  :set #'fstar-subp-set-keybinding-style
  :type '(choice (const :tag "Proof-General style bindings" pg)
                 (const :tag "Atom-style bindings" atom)))

;;;; Main entry point

(defun fstar-setup-interactive ()
  "Setup interactive F* mode."
