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

(make-local-variable 'fstar-subp-sloppy)

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

(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-interactive)


  :group 'fstar-interactive)

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

