Commit 1055fdb8 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Avoid using Queue.t for a one-shot data structure, especially an unordered one.

parent 158b262b
......@@ -402,32 +402,20 @@ let get_new_results ~blocking = (* TODO: handle ProverStarted events *)
let forward_results ~blocking =
get_new_results ~blocking;
let q = Queue.create () in
let q = ref [] in
Hashtbl.iter (fun key element ->
if element = ProverStarted && blocking then
()
else
Queue.push (ServerCall key, element) q) result_buffer;
q := (ServerCall key, element) :: !q) result_buffer;
Hashtbl.clear result_buffer;
q
!q
let query_result_buffer id =
try let r = Hashtbl.find result_buffer id in
Hashtbl.remove result_buffer id; r
with Not_found -> NoUpdates
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 editor_result ret = {
pr_answer = Unknown ("", None);
pr_status = ret;
......
......@@ -172,10 +172,8 @@ 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 forward_results: blocking:bool -> (prover_call * prover_update) list
(** returns new results from why3server, in an unordered fashion. *)
val query_call : prover_call -> prover_update
(** non-blocking function that reports any new updates
......
......@@ -377,19 +377,10 @@ let timeout_handler () =
was not launched so getting results could fail. *)
if Hashtbl.length prover_tasks_in_progress != 0 then begin
let results = Call_provers.forward_results ~blocking:S.blocking in
while not (Queue.is_empty results) do
let (call, prover_update) = Queue.pop results in
let c = try Some (Hashtbl.find prover_tasks_in_progress call)
with Not_found -> None in
match c with
| None -> () (* we do nothing. We probably received ProverStarted after
ProverFinished because what is sent to and received from
the server is not ordered. *)
| Some c ->
begin
let (ses,id,pr,callback,started,call,ores) = c in
match prover_update with
List.iter (fun (call, prover_update) ->
match Hashtbl.find prover_tasks_in_progress call with
| (ses,id,pr,callback,started,call,ores) ->
begin match prover_update with
| Call_provers.NoUpdates -> ()
| Call_provers.ProverStarted ->
assert (not started);
......@@ -413,8 +404,12 @@ let timeout_handler () =
if started then decr number_of_running_provers;
(* inform the callback *)
callback (InternalFailure (exn))
end
done
end
| exception Not_found -> ()
(* We probably received ProverStarted after ProverFinished,
because what is sent to and received from the server is
not ordered. *)
) results;
end;
(* When blocking is activated, we are in script mode and we don't want editors
......
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