 (defun fstar-jump-to-definition ()
   "Jump to definition of identifier at point, if any."
   (interactive)
-  (fstar-subp--ensure-available #'user-error 'info)
-  (fstar-subp--query (fstar-subp--positional-info-query (point))
-                (fstar-subp--info-wrapper #'fstar--jump-to-definition-continuation (point))))
+  (fstar-subp--ensure-available #'user-error 'lookup)
+  (fstar-subp--query (fstar-subp--positional-lookup-query (point))
+                (fstar-subp--lookup-wrapper #'fstar--jump-to-definition-continuation (point))))
 
 ;;;; Quick-peek
 
 (defun fstar--quick-peek-continuation (info)
   "Show type from INFO in inline pop-up."
   (if info
-      (let ((segments (delq nil (list (fstar-symbol-info-sig info)
-                                      (fstar-symbol-info-docstring info)))))
+      (let ((segments (delq nil (list (fstar-lookup-result-sig info)
+                                      (fstar-lookup-result-docstring info)))))
         (quick-peek-show (mapconcat #'identity segments "\n\n")
                          (car (with-syntax-table fstar--fqn-at-point-syntax-table
                                 (bounds-of-thing-at-point 'symbol)))))

  (format "| %s -> $$" (replace-regexp-in-string "\\`(\\(.*\\))\\'" "\\1" branch)))

(defun fstar--insert-match-continuation (type response)
  "Handle RESPONSE to a #show-match query.
TYPE is used in error messages"
  (-if-let* ((branches (and response
                            (if (fstar--has-feature 'interactive-json)
                                response
                              (split-string response "\n")))))
      (let* ((name-str (car branches))

(defun fstar-quick-peek ()
  "Toggle inline window showing type of identifier at point."
  (interactive)
  (fstar-subp--ensure-available #'user-error 'lookup)
  (when (= (quick-peek-hide) 0)
    (fstar-subp--query (fstar-subp--positional-lookup-query (point))
                  (fstar-subp--lookup-wrapper #'fstar--quick-peek-continuation (point)))))

;;;; Company

(defun fstar-subp--completion-query (prefix)
  "Prepare a `completions' query from PREFIX."
  (fstar-assert (not (string-match-p " " prefix)))
  (if (fstar--has-feature 'json-subp)
      (make-fstar-subp-query
       :query "autocomplete"
       :args `(("partial-symbol" . ,prefix)))
