 (defun fstar-subp-remove-issues-overlays ()
   "Remove all F* overlays in the current buffer."
   (mapcar #'delete-overlay (fstar-subp-issues-overlays)))
-
-(defmacro fstar-subp-with-process-buffer (proc &rest body)
-  "Move to PROC's buffer to eval BODY."
-  (declare (indent defun) (debug t))
-  `(-when-let* ((livep    (fstar-subp-live-p ,proc))
-                (buf      (process-buffer ,proc))
-                (buflivep (buffer-live-p buf)))
-     (with-current-buffer buf
-       ,@body)))
-
-(defmacro fstar-subp-with-source-buffer (proc &rest body)
-  "Move to parent buffer of PROC to eval BODY."
-  (declare (indent defun) (debug t))
-  `(-when-let* ((livep    (fstar-subp-live-p ,proc))
-                (buf      (process-get ,proc 'fstar-subp-source-buffer))
-                (buflivep (buffer-live-p buf)))
-     (with-current-buffer buf
-       ,@body)))
 
 (defun fstar-subp-find-response (proc)
   "Find full response in PROC's buffer; handle it if found."

      ;; 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 ()


(defun fstar-subp-killed (proc)
  "Clean up buffer after PROC was killed."
  (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 (&optional proc)
  "Kill F* subprocess PROC and clean up buffer."
  (interactive)
  (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)
  "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)))
