 ;; * Syntax highlighting
 ;; * Unicode math (with prettify-symbols-mode)
 ;; * Indentation
-;; * Real-time verification (with flycheck)
+;; * Real-time verification (requires the Flycheck package)
 ;; * Interactive proofs (à la Proof-General)
 ;;
 ;; See https://github.com/FStarLang/fstar-mode.el for setup and usage tips.

  :group 'languages)

;;; Flycheck

(flycheck-def-executable-var fstar "fstar.exe")

(defconst fstar-error-patterns
  (let ((fstar-pat '((message) "near line " line ", character " column " in file " (file-name)))

      (warning "WARNING: " ,@fstar-pat)
      (error ,@z3-pat))))

(when (featurep 'flycheck)
  (define-obsolete-variable-alias 'flycheck-fstar-executable 'fstar-executable "0.2")

  (flycheck-define-command-checker 'fstar
    "Flycheck checker for F*."
    :command '("fstar.exe" source-inplace)
    :error-patterns fstar-error-patterns
    :error-filter #'flycheck-increment-error-columns
    :modes '(fstar-mode))

  (add-to-list 'flycheck-checkers 'fstar))

(defun fstar-setup-flycheck ()
  "Prepare Flycheck for use with F*."
  (when (featurep 'flycheck)
    (flycheck-mode)))

;;; Customization

(defcustom fstar-executable "fstar.exe"
  "Full path to the fstar.exe binary."
  :group 'fstar
  :risky t)

;;; Build config

(defconst fstar-build-config-header "(*--build-config")
(defconst fstar-build-config-footer "--*)")

;;; Prettify symbols

