diff options
| author | gareuselesinge | 2013-10-11 09:10:52 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-10-11 09:10:52 +0000 |
| commit | 0f9a7d13714f30a3c1eeee41b6a500370e5c18bb (patch) | |
| tree | 2d23396a13e1d340382b56a49f8f92b48dfbddad /lib/vcs.mli | |
| parent | ce449695c310ddf495734ca370b42071890ddbfa (diff) | |
Vcs: the gc method returns the set of nodes that were collected
In this way one can post-process them. Stm can for example cancel
the ongoing jobs related to nodes that are no more there.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16877 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/vcs.mli')
| -rw-r--r-- | lib/vcs.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/lib/vcs.mli b/lib/vcs.mli index 72feae5dc4..6c3571a082 100644 --- a/lib/vcs.mli +++ b/lib/vcs.mli @@ -70,16 +70,17 @@ module type S = sig val set_info : ('k,'e,'info) t -> id -> 'info -> ('k,'e,'info) t val get_info : ('k,'e,'info) t -> id -> 'info option - val gc : ('k,'e,'info) t -> ('k,'e,'info) t - module NodeSet : Set.S with type elt = id + + (* Removes all unreachable nodes and returns them *) + val gc : ('k,'e,'info) t -> ('k,'e,'info) t * NodeSet.t val reachable : ('k,'e,'info) t -> id -> NodeSet.t (* read only dag *) module Dag : Dag.S with type node = id val dag : ('kind,'diff,'info) t -> ('diff,'info,id) Dag.t - + val create_cluster : ('k,'e,'i) t -> id list -> id -> ('k,'e,'i) t val cluster_of : ('k,'e,'i) t -> id -> id Dag.Cluster.t option val delete_cluster : ('k,'e,'i) t -> id Dag.Cluster.t -> ('k,'e,'i) t |