   "Return t if current `fstar-subp--process' is live and idle."
   (and (fstar-subp-live-p fstar-subp--process)
        (not fstar-subp--continuation)))
+
+(defun fstar-subp--ensure-available (error-fn)
+  "Raise an error with ERROR-FN if F* isn't available."
+  (when fstar-subp--continuation
+    (funcall error-fn "F* seems busy; please wait until processing is complete"))
+  (unless (fstar-subp-live-p)
+    (funcall error-fn "Please start F* before jumping to a definition")))
 
 (defun fstar-subp--query (query continuation)
   "Send QUERY to F* subprocess; handle results with CONTINUATION."


(defun fstar--jump-to-definition-continuation (info)
  "Jump to position in INFO."
  (pcase-let* ((target-fname (fstar-pos-info-source-file info))
               (`(,target-row . ,target-col) (fstar-pos-info-def-start info)))
    (fstar--save-point)
    (catch 'not-found
      (unless (equal target-fname "<input>")
        (unless (file-exists-p target-fname)
          (message "File not found: %S" target-fname)
          (throw 'not-found nil))
        (find-file target-fname))
      (fstar--goto target-row target-col)
      (recenter)
      (pulse-momentary-highlight-one-line (point)))))

(defun fstar-jump-to-definition ()
  "Jump to definition of identifier at point, if any."
  (interactive)
  (cond
   ((not fstar-compat--can-use-info)
    (user-error "This feature isn't available in F* < 0.9.4.1"))
   (fstar-subp--continuation
    (user-error "F* seems busy; please wait until processing is complete"))
   ((not (fstar-subp-live-p))
    (user-error "Please start F* before jumping to a definition"))
   (t (fstar-subp--query (fstar-subp--info-query (point))
                         (apply-partially #'fstar-subp--info-continuation
                                          #'fstar--jump-to-definition-continuation
                                          (point))))))

;;;; Starting the F* subprocess


    (modify-syntax-entry ?# "_" table)
    (modify-syntax-entry ?_ "_" table)
    (modify-syntax-entry ?' "_" table)
    ;; Punctuation
    (modify-syntax-entry ?. "." table)
    (modify-syntax-entry ?+ "." table)
    (modify-syntax-entry ?- "." table)
    (modify-syntax-entry ?= "." table)
    (modify-syntax-entry ?% "." table)
    (modify-syntax-entry ?< "." table)
    (modify-syntax-entry ?> "." table)
    (modify-syntax-entry ?& "." table)
    (modify-syntax-entry ?| "." table)
    ;; Comments and strings
    (modify-syntax-entry ?\\ "\\" table)
    (modify-syntax-entry ?\" "\"" table)
