 ;;; Indentation
 
 (defun fstar-comment-offset ()
+  "Compute offset at beginning of comment."
   (comment-normalize-vars)
   (when (fstar-in-comment-p)
     (save-excursion

  (font-lock-mode))

(defun fstar-teardown-font-lock ()
  (remove-from-invisibility-spec 'fstar-subscripts))

;;; Syntax table

           do (delete-overlay overlay)))

(defun fstar-subp-warn-unexpected-output (string)
  "Warn user about unexpected output STRING."
  (message "F*: received unexpected output from subprocess (%s)" string))

(defun fstar-subp-filter (proc string)
