Commit f2c4713b authored by MARCHE Claude's avatar MARCHE Claude

provide function [forward_results] in [Call_provers] API

parent c8a0ada9
* marks an incompatible change
Version 0.88.1, ?, 2017
===============================
API
o export function [forward_results] in [Call_prover] interface
Version 0.88.0, October 6, 2017
===============================
......
......@@ -398,6 +398,18 @@ let get_new_results ~blocking = (* TODO: handle ProverStarted events *)
Hashtbl.add result_buffer id x)
(wait_for_server_result ~blocking)
let forward_results ~blocking =
get_new_results ~blocking;
let q = Queue.create () in
Hashtbl.iter (fun key element ->
if element = ProverStarted && blocking then
()
else
Queue.push (ServerCall key, element) q) result_buffer;
Hashtbl.clear result_buffer;
q
let query_result_buffer id =
try let r = Hashtbl.find result_buffer id in
Hashtbl.remove result_buffer id; r
......
......@@ -163,6 +163,11 @@ type prover_update =
| ProverStarted
| ProverFinished of prover_result
val forward_results: blocking:bool -> (prover_call * prover_update) Queue.t
(** returns new results that are given by why3server. *)
val query_call : prover_call -> prover_update
(** non-blocking function that reports any new updates
from the server related to a given prover call. *)
......
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