 (defgroup fstar nil
   "F* mode."
   :group 'languages)
+
+(defgroup fstar-literate nil
+  "Literate programming support for F* mode."
+  :group 'fstar)
+
+(defgroup fstar-interactive nil
+  "Interactive proofs."
+  :group 'fstar)
+
+(defgroup fstar-tactics nil
+  "Tactics and tactic-based proofs."
+  :group 'fstar-interactive)
 
 (defcustom fstar-executable "fstar.exe"
   "Where to find F*.

(defface fstar-subp-overlay-lax-face
  '((t :slant italic))
  "Face used to highlight lax-checked sections of the buffer."
  :group 'fstar)

(defface fstar-subp-overlay-pending-face
  '((((background light)) :background "#AD7FA8")
    (((background dark))  :background "#5C3566"))
  "Face used to highlight pending sections of the buffer."
  :group 'fstar)

(defface fstar-subp-overlay-pending-lax-face
  '((t :inherit (fstar-subp-overlay-pending-face fstar-subp-overlay-lax-face)))
  "Face used to highlight pending lax-checked sections of the buffer."
  :group 'fstar)

(defface fstar-subp-overlay-busy-face
  '((((background light)) :background "mistyrose")
    (((background dark))  :background "mediumorchid"))
  "Face used to highlight busy sections of the buffer."
  :group 'fstar)

(defface fstar-subp-overlay-busy-lax-face
  '((t :inherit (fstar-subp-overlay-busy-face fstar-subp-overlay-lax-face)))
  "Face used to highlight busy lax-checked sections of the buffer."
  :group 'fstar)

(defface fstar-subp-overlay-processed-face
  '((((background light)) :background "#EAF8FF")
    (((background dark))  :background "darkslateblue"))
  "Face used to highlight processed sections of the buffer."
  :group 'fstar)

(defface fstar-subp-overlay-processed-lax-face
  '((t :inherit (fstar-subp-overlay-processed-face fstar-subp-overlay-lax-face)))
  "Face used to highlight processed lax-checked sections of the buffer."
  :group 'fstar)

(defface fstar-subp-overlay-error-face
  '((t :underline (:color "red" :style wave)))
  "Face used to highlight errors."
  :group 'fstar)

(defface fstar-subp-overlay-warning-face
  '((t :underline (:color "orange" :style wave)))
  "Face used to highlight warnings."
  :group 'fstar)

(defface fstar-subp-overlay-bullet-error-face
  '((t :foreground "red"))
  "Face used to color bullets indicating error locations."
  :group 'fstar)

(defface fstar-subp-overlay-bullet-warning-face
  '((t :foreground "orange"))
  "Face used to color bullets indicating warning locations."
  :group 'fstar)

(defmacro fstar-subp-with-process-buffer (proc &rest body)
  "If PROC is non-nil, move to PROC's buffer to eval BODY."


(defcustom fstar-interactive-keybinding-style 'pg
  "Which style of bindings to use in F* interactive mode."
  :group 'fstar-interactive
  :set #'fstar-subp-set-keybinding-style
  :type '(choice (const :tag "Proof-General style bindings" pg)
                 (const :tag "Atom-style bindings" atom)))
