 
 ;;; ;; ;; 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 `(("symbol" . ,(or (fstar--fqn-at-point pos) ""))
+       :args `(("context" . ,(symbol-name (or (fstar-subp--context-at-point) 'code)))
+               ("symbol" . ,(or (fstar--fqn-at-point pos) ""))
                ("requested-info" . ,fields)
                ("location" .
                 (("filename" . "<input>")

      (`sorted t)
      (`no-cache t)
      (`duplicates nil)
      (`match (get-text-property 0 'match arg))
      (`annotation (get-text-property 0 'annot arg))
      (`pre-render (fstar-subp-company--pre-render arg (car rest)))
      (`post-completion (fstar-subp-company--post-completion arg)))))

(defun fstar-setup-company ()


;;; ;; ;; Company

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

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

(defun fstar-subp-company--fontify-snippets-1 (match)
  "Compute prettified rendition of placeholder MATCH."
  (propertize (match-string 1 match) 'face '(bold italic)))

(defun fstar-subp-company--post-process-candidate (candidate)
  "Post-process and return CANDIDATE.
Post-processing includes fontification of snippets — one might
hope to do this in company's pre-render, but pre-render can't
change the length of a candidate."
  (if (string-match-p fstar-subp-company--snippet-re candidate)
      (propertize (replace-regexp-in-string
                   fstar-subp-company--snippet-re
                   #'fstar-subp-company--fontify-snippets-1
                   candidate)
                  'fstar--snippet candidate)
    candidate))

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

(defun fstar-subp-company-json--make-candidate (context record)
  "Extract a candidate from RECORD and tag it with CONTEXT."
  (pcase-let* ((`(,match-end ,annot ,candidate) record))
    (fstar--set-text-props
     candidate 'fstar--match-end match-end 'fstar--annot annot 'fstar--context context)
    (fstar-subp-company--post-process-candidate candidate)))

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

(defconst fstar-subp-company--ns-mod-annots
  '("mod" "ns" "+mod" "+ns" "(mod)" "(ns)" "-mod" "-ns"))

(defun fstar-subp-company--candidate-fqn (candidate context)
  "Compute the fully qualified name of CANDIDATE in CONTEXT."
  (let* ((ns (get-text-property 0 'fstar--annot candidate))
         (snippet (or (get-text-property 0 'fstar--snippet candidate) candidate)))
    (pcase context
      (`code
       (if (member ns (cons "" fstar-subp-company--ns-mod-annots))
           snippet
         (concat ns "." snippet)))
      ((or `set-options `reset-options)
       (replace-regexp-in-string " .*" "" snippet))
      ((or `open `include `module-alias `let-open)
       snippet))))

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