   (declare (indent 2))
   (if (fstar-subp-available-p)
       (fstar-subp--query
-       (fstar-subp--positionless-lookup-query
-           (fstar-subp-company--candidate-fqn candidate) fields)
+       (let* ((context (get-text-property 0 'fstar--context candidate))
+              (fqn (fstar-subp-company--candidate-fqn candidate context)))
+         (fstar-subp--positionless-lookup-query fqn fields context))
        (fstar-subp--lookup-wrapper nil continuation))
     (funcall continuation 'busy)))
 


;;; ;; ;; 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)))

(defconst fstar-subp-company--snippet-re "\\${\\(.+?\\)}")

(defun fstar-subp-company--post-process-candidate (candidate)
  "Post-process and return CANDIDATE."
  candidate)

(defun fstar-subp-company-legacy--prepare-candidate (line)
  "Extract a candidate from LINE."
  (pcase (split-string line " ")
    (`(,match-end ,annot ,candidate . ,_)
     (setq match-end (string-to-number match-end))
     (fstar--set-text-props candidate 'match match-end 'annot annot)
     (fstar-subp-company--post-process-candidate candidate))))

(defun fstar-subp-company-json--prepare-candidate (record)
  "Extract a candidate from RECORD."
  (pcase-let* ((`(,match-end ,annot ,candidate) record))
    (fstar--set-text-props candidate 'match match-end 'annot annot)
    (fstar-subp-company--post-process-candidate candidate)))

(defun fstar-subp-company--candidates-continuation (callback status response)
  "Handle the results (STATUS, RESPONSE) of an `autocomplete' query.
Return (CALLBACK CANDIDATES)."
  (pcase status
    ((or `failure `interrupted)
     (funcall callback nil))
    (`success
     (save-match-data
       (funcall callback
                (if (fstar--has-feature 'json-subp)
                    (mapcar #'fstar-subp-company-json--prepare-candidate response)
                  (delq nil (mapcar #'fstar-subp-company-legacy--prepare-candidate
                                    (split-string response "\n")))))))))

(defun fstar-subp--positionless-lookup-query (symbol fields)
  "Prepare a header for an info query for SYMBOL with FIELDS."
  (declare (indent 1))
  (when (equal symbol "")
    (user-error "Looking up an empty name"))
  (if (fstar--has-feature 'json-subp)
      (make-fstar-subp-query
       :query "lookup"
       :args `(("symbol" . ,symbol)
               ("requested-info" . ,fields)))
    (format "#info %s" symbol)))

(defun fstar-subp-company--candidate-fqn (candidate)
  "Compute the fully qualified name of CANDIDATE."
  (let* ((ns (get-text-property 0 'annot candidate)))
    (if (string= ns "") candidate
      (concat ns "." candidate))))

(defun fstar-subp-company--async-lookup (candidate fields continuation)
  "Pass info FIELDS about CANDIDATE to CONTINUATION.


;;; ;; ;; Lookup queries

(defconst fstar--command-line-option-prefix-re
  "--[-_.0-9A-Za-z]*")

(defun fstar-subp--context-at-point ()
  "Compute context at point.
Must be called with syntax table `fstar--fqn-at-point-syntax-table'"
  (let ((line-context
         (save-excursion
           (goto-char (point-at-bol))
           (cond
            ((looking-at-p "open ") 'open)
            ((looking-at-p "include ") 'include)
            ((looking-at-p "module \\(?:\\s_\\|\\sw\\)+ *=") 'module-alias)
            ((looking-at-p "#set-options") 'set-options)
            ((looking-at-p "#reset-options") 'reset-options)))))
    (cond
     ((memq line-context '(open include module-alias))
      line-context)
     ((memq line-context '(set-options reset-options))
      (when (looking-back fstar--command-line-option-prefix-re (point-at-bol))
        line-context))
     ((looking-back "\\_<let open [^ \n]*" (point-at-bol))
      'let-open)
     (t 'code))))

(defun fstar-subp--positional-lookup-query (pos fields)
  "Prepare a header for an info query at POS with FIELDS."
  (declare (indent 1))
  (if (fstar--has-feature 'json-subp)
      (make-fstar-subp-query
       :query "lookup"
       :args `(("context" . ,(symbol-name (or (fstar-subp--context-at-point) 'code)))
               ("symbol" . ,(or (fstar--fqn-at-point pos) ""))
               ("requested-info" . ,fields)
               ("location" .
                (("filename" . "<input>")
