        ((fstar-subp-status-eq overlay 'busy)
         (user-error "Cannot retract a busy section"))))))
 
+(defun fstar-subp--status-face (status lax)
+  "Get face for STATUS, optionally with LAX modifier."
+  (intern (format "fstar-subp-overlay-%s-%sface" (symbol-name status)
+                  (if lax "lax-" ""))))
+
 (defun fstar-subp-set-status (overlay status)
   "Set status of OVERLAY to STATUS."
   (fstar-assert (memq status fstar-subp-statuses))
   (let* ((inhibit-read-only t)
-         (face-name (format "fstar-subp-overlay-%s-%sface" (symbol-name status)
-                            (if (overlay-get overlay 'fstar-subp--lax) "lax-" ""))))
+         (lax (overlay-get overlay 'fstar-subp--lax))
+         (help-echo (propertize " " 'fstar--subp-legend (current-buffer))))
     (overlay-put overlay 'fstar-subp-status status)
     (overlay-put overlay 'priority -1)
-    (overlay-put overlay 'face (intern face-name))
+    (overlay-put overlay 'help-echo help-echo)
+    (overlay-put overlay 'face (fstar-subp--status-face status lax))
     (overlay-put overlay 'insert-in-front-hooks '(fstar-subp-overlay-attempt-modification))
     (overlay-put overlay 'modification-hooks '(fstar-subp-overlay-attempt-modification))))
 

  "Remove all F* overlays in the current buffer."
  (mapcar #'delete-overlay (fstar-subp-issue-overlays)))

;;;; Basic subprocess operations

(defun fstar-subp-live-p (&optional proc)

  :risky t)

(defconst fstar-known-modules
  '((font-lock      . "Syntax highlighting")
    (prettify       . "Unicode math (e.g. display forall as ∀; requires emacs 24.4 or later)")
    (indentation    . "Indentation (based on control points)")
    (comments       . "Comment syntax and special comments ('(***', '(*+', etc.)")
    (flycheck       . "Real-time verification (good for small files; requires Flycheck)")
    (interactive    . "Interactive verification (à la Proof-General)")
    (eldoc          . "Type annotations in the minibuffer.")
    (company        . "Completion with company-mode.")
    (overlay-legend . "Show a legend in the modeline when hovering an F* overlay."))
  "Available components of F*-mode.")

(defcustom fstar-enabled-modules
  '(font-lock prettify indentation comments interactive
              eldoc company overlay-legend)
  "Which F*-mode components to load."
  :group 'fstar
  :type `(set ,@(cl-loop for (mod . desc) in fstar-known-modules
