   "Face used to highlight warnings."
   :group 'fstar)
 
-(defvar fstar-subp-debug nil
-  "If non-nil, print debuging information in interactive mode.")
-
-(defun fstar-subp-toggle-debug ()
-  "Toggle `fstar-subp-debug'."
-  (interactive)
-  (message "F*: Debugging set to %s." (setq-local fstar-subp-debug (not fstar-subp-debug))))
-
-(defmacro fstar-subp-log (format &rest args)
-  "Log a message, conditional on fstar-subp-debug.
-
-FORMAT and ARGS are as in `message'."
-  (declare (debug t))
-  (let ((original-message (make-symbol "msg")))
-    `(when fstar-subp-debug
-       (let ((,original-message (current-message)))
-         (let ((inhibit-message t))
-           (message ,format ,@args))
-         (when ,original-message
-           (message "%s" ,original-message))))))
-
 (defmacro fstar-subp-with-process-buffer (proc &rest body)
   "If PROC is non-nil, move to PROC's buffer to eval BODY."
   (declare (indent defun) (debug t))


(defun fstar-subp-sentinel (proc signal)
  "Handle PROC's SIGNAL."
  (fstar-subp-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-filter (proc string)
  "Handle PROC's output (STRING)."
  (when string
    (fstar-log "OUTPUT [%s]" string)
    (if (fstar-subp-live-p proc)
        (fstar-subp-with-process-buffer proc
          (goto-char (point-max))
