From a2388b6ae2b3bf680d03487abac00787e50976f9 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Thu, 24 Oct 2013 15:41:38 +0000
Subject: Ephemeron: add a function to run a collection cycle

This is necessary if one wants to check how much memory
Coq uses after a collection.  The idiom is:
  Gc.full_major (); Ephemeron.clear (); Gc.full_major ();
since the first collection may just put collected ephemerons
in a to_be_cleared list that is processed by Ephemeron.get/create/clear.
Processing the list may create new garbage (the content of the ephemeron),
Hence a new Gc cycle has to be run afterwards.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16929 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/ephemeron.ml  | 2 ++
 lib/ephemeron.mli | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/lib/ephemeron.ml b/lib/ephemeron.ml
index ee763086c9..d4ce7b1eac 100644
--- a/lib/ephemeron.ml
+++ b/lib/ephemeron.ml
@@ -85,3 +85,5 @@ let iter_opt k f =
   with
   | None -> ()
   | Some v -> f v
+
+let clear () = run_collection ()
diff --git a/lib/ephemeron.mli b/lib/ephemeron.mli
index bc34c5c66f..c1ceb3fd97 100644
--- a/lib/ephemeron.mli
+++ b/lib/ephemeron.mli
@@ -48,3 +48,5 @@ val get : 'a key -> 'a
 (* These never fail. *)
 val iter_opt : 'a key -> ('a -> unit) -> unit
 val default : 'a key -> 'a -> 'a
+
+val clear : unit -> unit
-- 
cgit v1.2.3