Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
24933cd1
Commit
24933cd1
authored
Nov 06, 2017
by
Guillaume Melquiond
Browse files
Avoid using Queue.t for a one-shot data structure, especially an unordered one.
parent
69e8633a
Changes
2
Hide whitespace changes
Inline
Side-by-side
src/driver/call_provers.ml
View file @
24933cd1
...
...
@@ -400,15 +400,14 @@ 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
...
...
src/driver/call_provers.mli
View file @
24933cd1
...
...
@@ -163,10 +163,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
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment