   "Like `fstar-subp--parse-prover-args-1' on ARGSV, but infer VAR-NAME."
   `(fstar-subp--parse-prover-args-1 ,argsv ',argsv))
 
-(defun fstar-subp-get-prover-args ()
+(defun fstar-subp-get-prover-args (&optional no-ide)
   "Compute F*'s arguments.
 Function is public to make it easier to debug
 `fstar-subp-prover-args' and
-`fstar-subp-prover-additional-args'."
+`fstar-subp-prover-additional-args'.
+Non-nil NO-IDE means don't include `--ide' and `--in'."
   (let ((smt-path (fstar--maybe-cygpath (fstar-subp-find-smt-solver)))
-        (ide-flag (if (fstar--has-feature 'json-subp) "--ide" "--in"))
+        (ide-flag (if no-ide nil
+                    (if (fstar--has-feature 'json-subp) '("--ide") '("--in"))))
         (usr-args (append
                    (fstar-subp--parse-prover-args fstar-subp-prover-args)
                    (fstar-subp--parse-prover-args fstar-subp-prover-additional-args))))
-    `(,(fstar-subp--buffer-file-name) ,ide-flag "--smt" ,smt-path ,@usr-args)))
+    `(,(fstar-subp--buffer-file-name) ,@ide-flag "--smt" ,smt-path ,@usr-args)))
 
 (defun fstar-subp--prover-includes-for-compiler-hacking ()
   "Compute a list of folders to include for hacking on the F* compiler."

        (setq fstar-subp--continuations (make-hash-table :test 'equal))
        (when (fstar--has-feature 'json-subp)
          (fstar-subp--wait-for-features-list proc))))))

;;; ;; Keybindings


     ["Switch to reStructuredText mode"
      fstar-literate-fst2rst])
    ("Utilities"
     ["Verify current file on the command line"
      fstar-cli-verify]
     ["Copy error message at point"
      fstar-copy-help-at-point (fstar--check-help-at-point)])
    ["Configuration" fstar-customize]))
