             (find-file target-fname))
           (fstar--goto target-row target-col)
           (recenter)
-          (pulse-momentary-highlight-one-line (point))))
+          (when (fboundp 'pulse-momentary-highlight-one-line)
+            (pulse-momentary-highlight-one-line (point)))))
     (message "No definition found")))
 
 (defun fstar-jump-to-definition ()


(defun fstar-subp-issue-overlays-at (pt)
  "Find all -subp issues overlays at point PT."
  (-filter #'fstar-subp-issue-overlay-p (overlays-at pt t)))

(defun fstar-subp-tracking-overlay-p (overlay)
  "Return non-nil if OVERLAY is an fstar-subp tracking overlay."

  (tooltip-mode 1)
  ;; Must use advice, because tooltip mode aggressively resets
  ;; `show-help-function' to `tooltip-show-help'.
  (when (fboundp 'advice-add)
    (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."
  (when (fboundp 'advice-remove)
    (dolist (fn '(tooltip-show-help tooltip-show-help-non-mode))
      (advice-remove fn #'fstar-subp--overlay-legend-help-function))))

;;;; Basic subprocess operations

