   "Disable F*-related font-locking."
   (when (buffer-live-p fstar--scratchpad)
     (kill-buffer fstar--scratchpad)))
+
+;;; Subscripts
+
+(defconst fstar-subscripts--font-lock-spec
+  `(,(fstar--fl-conditional-matcher fstar-syntax-id-with-subscript #'fstar--in-code-p)
+    (1 '(face fstar-subscript-face display (raise -0.3)) append)))
+
+(defun fstar-setup-subscripts ()
+  "Setup pretty subscripts."
+  (font-lock-add-keywords nil (list fstar-subscripts--font-lock-spec) 'append))
+
+(defun fstar-teardown-subscripts ()
+  "Teardown pretty subscripts."
+  (font-lock-remove-keywords nil (list fstar-subscripts--font-lock-spec)))
 
 ;;; Syntax table
 

      ("!"
       (0 'fstar-dereference-face))
      (,(fstar--fl-conditional-matcher "[{}]" #'fstar--in-code-p)
       (0 'fstar-braces-face append))
      (,(fstar--fl-conditional-matcher fstar-syntax-id-with-subscript #'fstar--in-code-p)
       (1 '(face fstar-subscript-face display (raise -0.3)) append)))))

(defconst fstar--scratchpad-name " *%s-scratchpad*")


  "Available components of F*-mode.")

(defcustom fstar-enabled-modules
  '(font-lock prettify subscripts indentation comments flycheck interactive
              eldoc company company-defaults spinner notifications
              literate overlay-legend tool-bar auto-insert)
  "Which F*-mode components to load."
