   (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.")
+    (message "F*: subprocess exited.")
     (fstar-subp-with-source-buffer proc
       (fstar-subp-killed))))
 

(defun fstar-subp-toggle-debug ()
  "Toggle `fstar-subp-debug'."
  (interactive)
  (message "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.

           unless (fstar-subp-status-eq overlay 'processed)
           do (delete-overlay overlay)))

(defun fstar-subp-warn-unexpected-output (string)
  "Warn user about unexpected output STR."
  (message "F*: received unexpected output from subprocess (%s)" string))

(defun fstar-subp-filter (proc string)
  "Handle PROC's output (STRING)."
  (when string
    (fstar-subp-log "OUTPUT [%s]" string)
    (if (fstar-subp-live-p proc)
        (fstar-subp-with-process-buffer proc
          (goto-char (point-max))
          (insert string)
          (fstar-subp-find-response proc))
      (run-with-timer 0 nil #'fstar-subp-warn-unexpected-output string))))

(defun fstar-subp-buffer-killed ()
  "Kill F* process associated to current buffer."
