 (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-literate-comment-face
  '((t :inherit default))
  "Face used for literate comments (///)."
  :group 'fstar)

(defface fstar-literate-gutter-face
  '((t :inverse-video t :inherit font-lock-comment-face))
  "Face used for the fringe next to literate comments (///)."
  :group 'fstar)

(defconst fstar-comment-start-skip "\\(//+\\|(\\*+\\)[ \t]*")


;; (defface fstar-literate-tty-gutter-face
;;   '((((type tty)) :inherit fstar-literate-gutter-face))
;;   "Face used for the gutter next to literate comments (///) on TTYs."
;;   :group 'fstar-literate)

(defconst fstar-literate--gutter-font-lock-props
  '(face fstar-literate-gutter-face display (space :width (+ (0) 0.5))))
