 
 ;;; ;; Killing Z3
 
+;; FIXME get rid of the process enumeration code now that we can just simply
+;; send a sigint to F*
+
 (defconst fstar--ps-line-regexp
   "^ *\\([0-9]+\\) +\\([0-9]+\\) \\(.+\\) *$")
 

    ("C-c C-b"        "C-S-b" fstar-subp-advance-to-point-max-lax)
    ("C-c C-r"        "C-S-r" fstar-subp-reload-to-point)
    ("C-c C-x"        "C-M-c" fstar-subp-kill-one-or-many)
    ("C-c C-c"        "C-M-S-c" fstar-subp-kill-z3))
  "Proof-General and Atom bindings table.")

(defun fstar-subp-refresh-keybinding (bind target unbind)

                       (string-suffix-p "z3.exe" cmd)))
          (signal-process pid 'int)
          (message "Sent SIGINT to %S (%S)" pid cmd))))))

(defun fstar-subp--interrupt-fstar ()
  "Interrupt the current F* computation."
  (when (or (not (fstar-subp-live-p)) (fstar-subp-available-p))
    (user-error "No busy F* process to interrupt"))
  (signal-process (process-id fstar-subp--process) 'int))

(defun fstar-subp-interrupt ()
  "Interrupt the current F* computation.
On older versions of F*, try to interrupt the underlying Z3
process — this is unreliable."
  (interactive)
  (if (fstar--has-feature 'interrupt)
      (fstar-subp--interrupt-fstar)
    (message "Consider upgrading to the latest F* to get reliable interrupts")
    (fstar-subp-kill-z3 nil)))

;;; ;; Parsing and display issues

