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

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

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

  :group 'fstar
  :type 'alist)

(defun fstar--same-ish-syntax (other ref)
  "Check if the syntax class of OTHER is similar to that of REF."
  (memq (char-syntax (or other ?\s))
        (if (memq (char-syntax ref) '(?w ?_))
            '(?w ?_)
          '(?. ?\\))))

(defun fstar--prettify-symbols-predicate (start end &optional _match)
  "Decide whether START..END should be prettified.
Differs from `prettify-symbols-default-compose-p' inasmuch as it
allows composition in code comments."
  (and (not (fstar--same-ish-syntax (char-before start) (char-after start)))
       (not (fstar--same-ish-syntax (char-after end) (char-before end)))
       ;; Test both endpoints because `syntax-ppss' doesn't include comment
       ;; openers in comments (i.e. the ‘*’ of ‘(*’ isn't in the comment).
       (fstar--in-code-p start)
       (fstar--in-code-p end)))

(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))
    (when (boundp 'prettify-symbols-compose-predicate)
      (setq prettify-symbols-compose-predicate #'fstar--prettify-symbols-predicate))
    (prettify-symbols-mode)))

;;; Font-Lock
