   :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."))
+  '((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)
+  '(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


(defun fstar-subp-company--async-info (candidate continuation)
  "Pass info about CANDIDATE to CONTINUATION.
If F* is busy, call CONTINUATION directly with BUSY."
  (if (fstar-subp-available-p)
      (fstar-subp--query
       (fstar-subp--positionless-info-query (fstar-subp-company--candidate-fqn candidate))

  (fstar-subp-set-status overlay 'busy)
  (let ((lax (overlay-get overlay 'fstar-subp--lax)))
    (fstar-subp-send-region (overlay-start overlay) (overlay-end overlay) lax
                       (apply-partially #'fstar-subp--overlay-continuation overlay))))

(defun fstar-subp-process-queue (buffer)
  "Process the next pending overlay of BUFFER, if any."
