Commit 5a5b51fd authored by Pierre-Yves Strub's avatar Pierre-Yves Strub Committed by MARCHE Claude
Browse files

OCaml API for provers interruption.

parent 4c518b2d
...@@ -513,6 +513,13 @@ let query_call = function ...@@ -513,6 +513,13 @@ let query_call = function
if pid = 0 then NoUpdates else if pid = 0 then NoUpdates else
ProverFinished (editor_result ret) ProverFinished (editor_result ret)
let interrupt_call = function
| ServerCall id ->
Prove_client.send_interrupt ~id
| EditorCall pid ->
(try Unix.kill pid Sys.sigkill with Unix.Unix_error _ -> ())
let rec wait_on_call = function let rec wait_on_call = function
| ServerCall id as pc -> | ServerCall id as pc ->
begin match query_result_buffer id with begin match query_result_buffer id with
...@@ -551,5 +558,3 @@ let call_editor ~command fin = ...@@ -551,5 +558,3 @@ let call_editor ~command fin =
let pid = Unix.create_process exec argarray fd_in Unix.stdout Unix.stderr in let pid = Unix.create_process exec argarray fd_in Unix.stdout Unix.stderr in
if use_stdin then Unix.close fd_in; if use_stdin then Unix.close fd_in;
EditorCall pid EditorCall pid
let interrupt_call id = Prove_client.send_interrupt ~id
...@@ -177,7 +177,8 @@ val query_call : prover_call -> prover_update ...@@ -177,7 +177,8 @@ val query_call : prover_call -> prover_update
(** non-blocking function that reports any new updates (** non-blocking function that reports any new updates
from the server related to a given prover call. *) from the server related to a given prover call. *)
val interrupt_call : prover_call -> unit
(** non-blocking function that asks for prover interruption *)
val wait_on_call : prover_call -> prover_result val wait_on_call : prover_call -> prover_result
(** blocking function that waits until the prover finishes. *) (** blocking function that waits until the prover finishes. *)
val interrupt_call : int -> unit
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment