                 (fstar-subp--pos-check-wrapper (point)
                   (apply-partially #'fstar--insert-match-continuation type))))
 
-(defun fstar--destruct-var-continuation (from to type response)
-  "Replace FROM..TO (with TYPE) with match from RESPONSE."
-  (pcase (and response (split-string response "\n"))
+(defun fstar--destruct-var-continuation (from to type status response)
+  "Replace FROM..TO (with TYPE) with match from RESPONSE.
+STATUS is the original query's status."
+  (pcase (and (eq status 'success) (split-string response "\n"))
     (`nil
      (message "No match found for type `%s'." type))
     (`(,_name ,branch)

    (dolist (opt-info options)
      (fstar-subp--list-options-1 display-default sp1 sp2 nl opt-info))))

(defun fstar-subp--list-options-continuation (source-buf response)
  "Let user jump to one of the dependencies in RESPONSE.
SOURCE-BUF indicates where the query was started from."
  (if response
      (let-alist response
        (with-help-window fstar--list-options-buffer-name
          (with-current-buffer standard-output


(defun fstar-subp--pos-check-wrapper (pos continuation)
  "Construct a continuation that runs CONTINUATION if point is POS.
Otherwise, call CONTINUATION with nil.  If POS is nil, the POS
check is ignored."
  (declare (indent 1))
  (lambda (status response)
    (if (or (null pos) (eq (point) pos))
        (funcall continuation status response)
      (funcall continuation 'interrupted nil))))

(defun fstar-subp--lookup-wrapper (pos continuation)
  "Handle the results of a lookup query at POS.
