   "Like `syntax-ppss' at POS, but don't move point."
   (when (buffer-narrowed-p)
     (warn "`syntax-ppss' called in narrowed buffer.
-Please submit the following stack-trace to the fstar-mode bug tracker:
+Please submit the following stack trace to the fstar-mode bug tracker:
 %s" (with-output-to-string (backtrace))))
   (save-excursion (syntax-ppss pos)))
 

  :group 'fstar
  :type 'alist)

(defun fstar-setup-prettify ()
  "Setup prettify-symbols for use with F*."
  (when (and (boundp 'prettify-symbols-alist)
             (fboundp 'prettify-symbols-mode))
    (setq-local prettify-symbols-alist (append fstar-symbols-alist
                                               prettify-symbols-alist))
    (prettify-symbols-mode)))

;;; Font-Lock

  (save-excursion
    (move-to-column column)
    (fstar-in-comment-p)))

(defun fstar--delimited-by-p (delim pos limit)
  "Check if POS is enclosed in DELIM before LIMIT."
  (let ((found nil))
    (while (and (setq pos (ignore-errors (scan-lists pos -1 1)))
                (< limit pos)
                (not (setq found (eq (char-after pos) delim)))))
    found))

(defun fstar--in-code-p (&optional pos)
  "Check if POS is in a code fragment (possibly embedded in a comment)."
  (let* ((sx (fstar--syntax-ppss (point)))
         (in-comment (nth 4 sx)))
    (or (not in-comment)
        (save-excursion
          (when pos (goto-char pos))
          (let ((comment-beg (nth 8 sx)))
            (fstar--delimited-by-p ?\[ (point) (max comment-beg (point-at-bol))))))))

(defun fstar-subp--column-number-at-pos (pos)
  "Return column number at POS."
