 
 (defun fstar-subp-sentinel (proc signal)
   "Handle PROC's SIGNAL."
-  (fstar-subp-log "SENTINEL [%s] [%s]" signal (process-status proc))
+  (fstar-log "SENTINEL [%s] [%s]" signal (process-status proc))
   (when (or (memq (process-status proc) '(exit signal))
             (not (process-live-p proc)))
     (message "F*: subprocess exited.")


(defun fstar-subp--query (query continuation)
  "Send QUERY to F* subprocess; handle results with CONTINUATION."
  (fstar-subp-log "QUERY [%s]" query)
  (fstar-assert (not fstar-subp--continuation))
  (setq fstar-subp--continuation continuation)
  (fstar-subp-start)

  :group 'fstar
  :type `(set ,@(cl-loop for (mod . desc) in fstar-known-modules
                         collect `(const :tag ,desc ,mod))))

;;; Debugging

(defvar fstar-debug nil
  "If non-nil, print debuging information in interactive mode.")

(defun fstar-toggle-debug ()
  "Toggle `fstar-debug'."
  (interactive)
  (message "F*: Debugging %s."
           (if (setq-default fstar-debug (not fstar-debug)) "enabled" "disabled")))

(define-obsolete-variable-alias 'fstar-subp-debug 'fstar-debug "0.4")
(define-obsolete-function-alias 'fstar-subp-toggle-debug 'fstar-toggle-debug "0.4")

(defun fstar--log (format &rest args)
  "Log a message, conditional on `fstar-debug'.

FORMAT and ARGS are as in `message'."
  (with-current-buffer (get-buffer-create "*fstar-debug*")
    (goto-char (point-max))
    (insert (apply #'format format args) "\n")))

(defmacro fstar-log (format &rest args)
  "Log a message, conditional on `fstar-debug'.

FORMAT and ARGS are as in `message'."
  (declare (debug t))
  `(when fstar-debug
     (fstar--log ,format ,@args)))

;;; Compatibility across F* versions

