Module Operation_pool.Prioritized

Pool of prioritized operations

Same record fields as type pool, but with a different set base

val of_pool : pool -> t

of_pool pool transforms pool into a prioritized pool of operations of low priority.

merge_external_operations ?initial_priority pool extern_ops creates a prioritized pool from a pool and extern_ops coming from an external source, which we prioritize.

Priorities for these operations is given according to the order of the list. The first element of the list has highest priority.

val add_operations : t -> Prioritized_operation.t list -> t