diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/future.ml | 1 | ||||
| -rw-r--r-- | lib/future.mli | 1 | ||||
| -rw-r--r-- | lib/remoteCounter.ml | 3 | ||||
| -rw-r--r-- | lib/remoteCounter.mli | 3 | ||||
| -rw-r--r-- | lib/stateid.ml | 9 | ||||
| -rw-r--r-- | lib/stateid.mli | 10 |
6 files changed, 27 insertions, 0 deletions
diff --git a/lib/future.ml b/lib/future.ml index 6ebbd4b1d6..4437cec848 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -41,6 +41,7 @@ module UUID = struct end module UUIDMap = Map.Make(UUID) +module UUIDSet = Set.Make(UUID) type 'a assignement = [ `Val of 'a | `Exn of exn | `Comp of 'a computation] diff --git a/lib/future.mli b/lib/future.mli index 18b0141329..a03823af82 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -61,6 +61,7 @@ module UUID : sig end module UUIDMap : Map.S with type key = UUID.t +module UUIDSet : Set.S with type elt = UUID.t exception NotReady diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml index 72887b21ac..c0217b22e5 100644 --- a/lib/remoteCounter.ml +++ b/lib/remoteCounter.ml @@ -37,6 +37,9 @@ let new_counter ~name a ~incr ~build = let backup () = !counters +let snapshot () = + List.map (fun (n,v) -> n, Obj.repr (ref (ref !!(Obj.obj v)))) !counters + let restore l = List.iter (fun (name, data) -> assert(List.mem_assoc name !counters); diff --git a/lib/remoteCounter.mli b/lib/remoteCounter.mli index 5a47ba6633..18e6b6b593 100644 --- a/lib/remoteCounter.mli +++ b/lib/remoteCounter.mli @@ -20,4 +20,7 @@ val new_counter : name:string -> type remote_counters_status val backup : unit -> remote_counters_status +(* like backup but makes a copy so that further increment does not alter + * the snapshot *) +val snapshot : unit -> remote_counters_status val restore : remote_counters_status -> unit diff --git a/lib/stateid.ml b/lib/stateid.ml index 09cc2b7e8f..59cf206e2e 100644 --- a/lib/stateid.ml +++ b/lib/stateid.ml @@ -39,3 +39,12 @@ let compare = Int.compare module Set = Set.Make(struct type t = int let compare = compare end) +type ('a,'b) request = { + exn_info : t * t; + stop : t; + document : 'b; + loc : Loc.t; + uuid : 'a; + name : string +} + diff --git a/lib/stateid.mli b/lib/stateid.mli index 11fac7a924..341544a678 100644 --- a/lib/stateid.mli +++ b/lib/stateid.mli @@ -33,3 +33,13 @@ val of_xml : xml -> t * The initial_state_id is assumed to be safe. *) val add : exn -> ?valid:t -> t -> exn val get : exn -> (t * t) option + +type ('a,'b) request = { + exn_info : t * t; + stop : t; + document : 'b; + loc : Loc.t; + uuid : 'a; + name : string +} + |