     `(,(propertize " " 'display '(space :align-to 0)) ;; 'face 'fringe
       ,(propertize "Legend: " 'face nil)
       ,(mapconcat
-        (pcase-lambda (`(,label . ,face))
-          (propertize (concat "​" sp "​" label "​" sp "​")
-                      'face face))
+        (lambda (label-face)
+          (propertize (concat "​" sp "​" (car label-face) "​" sp "​")
+                      'face (cdr label-face)))
         `(("pending" . (fstar-subp-overlay-pending-face))
           ("busy" . (fstar-subp-overlay-busy-face))
           ("processed" . (fstar-subp-overlay-processed-face))

  (tooltip-mode 1)
  ;; Must use advice, because tooltip mode aggressively resets
  ;; `show-help-function' to `tooltip-show-help'.
  (dolist (fn '(tooltip-show-help tooltip-show-help-non-mode))
    (advice-add fn :around #'fstar-subp--overlay-legend-help-function)))

(defun fstar-teardown-overlay-legend ()
  "Disable overlay legends in modeline."
  (dolist (fn '(tooltip-show-help tooltip-show-help-non-mode))
    (advice-remove fn #'fstar-subp--overlay-legend-help-function)))

;;;; Basic subprocess operations


  ;; Add-function doesn't work on 'eldoc-documentation-function in Emacs < 25,
  ;; due to the default value being nil instead of `ignore'.
  (setq-local eldoc-documentation-function #'fstar--eldoc-function)
  (when (fboundp 'advice-add)
    (advice-add 'eldoc-message :around #'fstar--eldoc-truncate-message))
  (eldoc-mode))

(defun fstar-teardown-eldoc ()
  "Tear down eldoc support."
  (kill-local-variable 'eldoc-documentation-function)
  (when (fboundp 'advice-remove)
    (advice-remove 'eldoc-message #'fstar--eldoc-truncate-message)))

;;;; xref-like features

