   "Face used to highlight decreases clauses."
   :group 'fstar)
 
+(defface fstar-subscript-underscore-face
+  '((t :height 0.4))
+  "Face used to highlight underscores before subscripts."
+  :group 'fstar)
+
 (defface fstar-subscript-face
-  '((t :height 0.8))
-  "Face used to use for subscripts"
+  '((t :height 1.0))
+  "Face used to highlight subscripts"
   :group 'fstar)
 
 (defface fstar-braces-face

      ,@fstar-syntax-additional)
     nil nil))
  (font-lock-set-defaults)
  (add-to-invisibility-spec 'fstar-subscripts)
  (add-to-list 'font-lock-extra-managed-props 'display)
  (add-to-list 'font-lock-extra-managed-props 'invisible)
  (font-lock-mode))

       (0 'fstar-dereference-face))
      ("[{}]"
       (0 'fstar-braces-face append))
      (,fstar-syntax-id-with-subscript
       ;; (1 '(face fstar-subscript-underscore-face invisible 'fstar-subscripts) prepend)
       (1 '(face fstar-subscript-face display (raise -0.3)) append)))))

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

