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

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

(defun fstar-subp-company-candidates (prefix &optional kind)
  "Compute candidates for PREFIX of kind KIND.
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 kind) 0.03)))
    (pcase retv
      (`(t . (,status ,results))
       (fstar-subp-company--candidates-continuation #'identity status results))
      (`(needs-callback . ,_)
       `(:async . ,(lambda (cb)
                     (setf (cdr retv)
                           (apply-partially
                            #'fstar-subp-company--candidates-continuation cb))))))))

(defun fstar-subp-company--completion-kind-at-point ()
  "Compute kind of prefix at point.
Must be called with syntax table `fstar--fqn-at-point-syntax-table'"
  (or (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")))
      (and (looking-back "\\_<let open \\(?:\\s_\\|\\sw\\)*" (point-at-bol)) "let-open")
      "symbol"))

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

(defun fstar-subp-company--pre-render (str annotation-p)
  "Propertize STR before displaying it.
ANNOTATION-P indicates where STR will be displayed."
  (if (and (not annotation-p)
           (string-match fstar-subp-company--snippet-re str))
      (replace-regexp-in-string
       fstar-subp-company--snippet-re #'fstar-subp-company--pre-render-1 str)
    str))

(defun fstar-subp-company--post-completion (candidate)
  "Run post-completion action for CANDIDATE."
  (when (string-match fstar-subp-company--snippet-re candidate)
    (fstar--expand-snippet candidate (- (point) (length candidate)) (point))))

(defun fstar-subp-company-backend (command &optional arg &rest rest)
  "Company backend for F*.

  (when (eq id 'interactive)
    (setq id (fstar--read-string "Show docs for%s: " (fstar--fqn-at-point))))
  (fstar-subp--query (fstar-subp--positionless-lookup-query id
                  '(type defined-at documentation) 'symbol-only)
                (fstar-subp--lookup-wrapper (point)
                  #'fstar--doc-at-point-continuation)))

