From 9a9a8ab4c2a07aa8faa04f50d6250930220b5be5 Mon Sep 17 00:00:00 2001
From: ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sun, 12 May 2013 15:33:27 +0000
Subject: Added a generic notion of hook. Hooks are functions to be set exactly
 once at runtime, often to reduce the mutual dependency of modules. This
 module permits to track them more easily.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16509 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/hook.ml | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)
 create mode 100644 lib/hook.ml

(limited to 'lib/hook.ml')

diff --git a/lib/hook.ml b/lib/hook.ml
new file mode 100644
index 000000000..ee468269f
--- /dev/null
+++ b/lib/hook.ml
@@ -0,0 +1,32 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+type 'a content =
+| Unset
+| Default of 'a
+| Set of 'a
+
+type 'a t = 'a content ref
+
+type 'a value = 'a t
+
+let get (hook : 'a value) = match !hook with
+| Unset -> assert false
+| Default data | Set data -> data
+
+let set (hook : 'a t) data = match !hook with
+| Unset | Default _ -> hook := Set data
+| Set _ -> assert false
+
+let make ?default () =
+  let data = match default with
+  | None -> Unset
+  | Some data -> Default data
+  in
+  let ans = ref data in
+  (ans, ans)
-- 
cgit v1.2.3