 (defvaralias 'flycheck-fstar-executable 'fstar-executable)
 (make-obsolete-variable 'flycheck-fstar-executable 'fstar-executable "0.2" 'set)
 
-(defun fstar--flycheck-enabled (checker)
-  "Check whether CHECKER should be used."
-  (eq fstar-flycheck-checker checker))
-
 (defun fstar--flycheck-verify-enabled (checker)
   "Create a verification result announcing whether CHECKER is enabled."
-  (list
-   (flycheck-verification-result-new
-    :label "Checker selection"
-    :message (if (fstar--flycheck-enabled checker) "OK, checker selected."
-               (format "Set ‘fstar-flycheck-checker’ \
+  (let ((enabled (eq fstar-flycheck-checker checker)))
+    (list
+     (flycheck-verification-result-new
+      :label "Checker selection"
+      :message (if enabled "OK, checker selected."
+                 (format "Set ‘fstar-flycheck-checker’ \
 to ‘%S’ to use this checker." checker))
-    :face (if (fstar--flycheck-enabled checker) 'success '(bold error)))))
+      :face (if enabled 'success '(bold error))))))
 
 (flycheck-define-command-checker 'fstar
   "Flycheck checker for F*."

  "Create a verification result announcing availability of the F* subprocess."
  (list
   (flycheck-verification-result-new
    :label "Subprocess running"
    :message (if (fstar-subp-live-p) "OK, F* started."
               "This checker requires a running F* subprocess.")
    :face (if (fstar-subp-live-p) 'success '(bold error)))
   (flycheck-verification-result-new
    :label "Subprocess started"
    :message (if (fstar-subp-available-p) "OK, F* idle."
               "This checker only runs when the F* subprocess is idle.")
    :face (if (fstar-subp-available-p) 'success '(bold error)))))

;;; Literate F*

(defconst fstar-literate--point-marker
  "<<<'P'O'I'N'T'>>>")

(defun fstar-literate--run-converter (&rest args)
  "Run converter with ARGS on current buffer.
