              (when (fstar--in-code-p)
                (substring-no-properties prefix))))))
       (`candidates
-       (fstar-subp-company-candidates arg))
+       (fstar-subp-company-candidates arg (fstar-subp-company--completion-kind-at-point)))
       (`meta
        `(:async . ,(apply-partially #'fstar-subp-company--async-meta arg)))
       (`doc-buffer

  (fstar-subp-company--async-lookup candidate '(defined-at)
    (apply-partially #'fstar-subp-company--location-continuation callback)))

(defun fstar-subp-company-candidates (prefix)
  "Compute candidates for PREFIX.
Briefly tries to get results synchronously to reduce flicker (see
URL https://github.com/company-mode/company-mode/issues/654), and
then returns an :async cons, as required by company-mode."
  (let ((retv (fstar-subp--query-and-wait (fstar-subp--completion-query prefix) 0.03)))
    (pcase retv
      (`(t . (,status ,results))
       (fstar-subp-company--candidates-continuation #'identity status results))


;;; ;; ;; Company

(defun fstar-subp--completion-query (prefix &optional kind)
  "Prepare a `completions' query from PREFIX of kind KIND."
  (fstar-assert (not (string-match-p " " prefix)))
  (if (fstar--has-feature 'json-subp)
      (make-fstar-subp-query
       :query "autocomplete"
       :args `(("partial-symbol" . ,prefix)
               ("kind" . ,kind)))
    (format "#completions %s #" prefix)))

(defun fstar-subp-company-legacy--prepare-candidate (line)
