 
 (defun fstar-subp-killed (proc)
   "Clean up buffer after PROC was killed."
-  (-when-let* ((procp proc)
-               (buf   (process-buffer proc))
-               (bufp  (buffer-live-p buf)))
-    (kill-buffer buf))
+  (fstar-subp-with-process-buffer proc nil
+    (kill-buffer))
   (fstar-subp-remove-tracking-overlays)
   (fstar-subp-remove-issues-overlays)
   (setq fstar-subp--busy-now nil
         fstar-subp--process nil))
 
-(defun fstar-subp-kill ()
-  "Kill F* subprocess and clean up buffer."
+(defun fstar-subp-kill (&optional proc)
+  "Kill F* subprocess PROC and clean up buffer."
   (interactive)
-  (when (fstar-subp-live-p)
-    (kill-process fstar-subp--process)
-    (accept-process-output fstar-subp--process 0.25 nil t))
-  (fstar-subp-killed fstar-subp--process))
+  (setq proc (or proc fstar-subp--process))
+  (when (fstar-subp-live-p proc)
+    (kill-process proc)
+    (accept-process-output proc 0.25 nil t))
+  (fstar-subp-with-source-buffer proc nil
+    (fstar-subp-killed proc)))
 
 (defun fstar-subp-sentinel (proc signal)
-  "Hamdle signals from PROC."
+  "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)))

      ;; string-trim is defined by flycheck if not present
      (fstar-subp-log "RESPONSE [%s] [%s]" status response)
      (delete-region resp-beg resp-real-end)
      (fstar-subp-with-source-buffer proc
        (fstar-subp-process-response status response)))))

(defun fstar-subp-clear-issues ()

  "Handle PROC's output (STRING)."
  (when string
    (fstar-subp-log "OUTPUT [%s]" string)
    (fstar-subp-with-process-buffer proc t
      (goto-char (point-max))
      (insert string)
      (fstar-subp-find-response proc))))

(defun fstar-subp-buffer-killed ()
  "Kill F* process associated to current buffer."
  (-when-let* ((proc (get-buffer-process (current-buffer))))
    (run-with-timer 0 nil #'fstar-subp-kill proc)))

(defun fstar-subp-make-buffer ()
  "Create a buffer for the F* subprocess."
  (with-current-buffer (generate-new-buffer
                        (format " *F* interactive for %s" (buffer-name)))
    (add-hook 'kill-buffer-hook #'fstar-subp-buffer-killed t t)
    (buffer-disable-undo)
    (current-buffer)))

