 (defun fstar-subp--completion-query (prefix)
   "Prepare a #completions query from PREFIX."
   (fstar-assert (not (string-match-p " " prefix)))
-  (format "#completions %s #\n" prefix))
+  (format "#completions %s #" prefix))
 
 (defun fstar-subp-company--parse-candidate (line)
   "Extract a candidate from LINE."

(defun fstar-subp--positional-info-query (pos)
  "Prepare a header for an info query at POS."
  (if (fstar--has-feature 'info-includes-symbol)
      (format "#info %s <input> %d %d\n"
              (or (fstar--fqn-at-point pos) "")
              (line-number-at-pos pos)
              (fstar-subp--column-number-at-pos pos))
    (format "#info <input> %d %d\n"
            (line-number-at-pos pos)
            (fstar-subp--column-number-at-pos pos))))


(defconst fstar-subp--failure "nok")
(defconst fstar-subp--done "\n#done-")

(defconst fstar-subp--cancel "#pop")
(defconst fstar-subp--footer "\n#end #done-ok #done-nok")

(defconst fstar-subp-statuses '(pending busy processed))

