 asynchronously after the fact)."
   (-if-let* ((hole-info (get-text-property (point) 'fstar--match-var-type)))
       (format "This hole has type `%s'" (car hole-info))
-    (when (and (fstar--has-feature 'info) (fstar-subp-available-p)
+    (when (and (fstar-subp--has-feature 'lookup) (fstar-subp-available-p)
                (not (fstar-subp--in-issue-p (point))))
       (let* ((query (fstar-subp--positional-info-query (point)))
              (retv (fstar-subp--query-and-wait query 0.01)))

  "Raise an error with ERROR-FN if F* isn't available.
Also raise an error if current subprocess doesn't meet version requirements for
FEATURE, if specified."
  (when feature
    (fstar--has-feature feature error-fn))
  (when (fstar-subp--busy-p)
    (funcall error-fn "F* seems busy; please wait until processing is complete"))
  (unless (fstar-subp-live-p)
    (funcall error-fn "Please start F* before jumping to a definition")))

(defun fstar-subp--serialize-query (query id)
  "Serialize QUERY with ID to JSON."

  (let ((header (format "[F* %s] " level)))
    (setq contents (string-trim contents))
    (message "%s" (replace-regexp-in-string "^" header contents))))

(defun fstar-subp--process-protocol-info (_vernum features)
  "Register information (VERNUM and FEATURES) about the current protocol."
  (setq features (mapcar 'intern features))
  (setq-local fstar-subp--features features)
  (fstar-subp-with-process-buffer fstar-subp--process
    (setq-local fstar-subp--features features)))

(defun fstar-subp--process-response (id status response)
  "Process STATUS and RESPONSE for query ID from F* subprocess."
