diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-12 15:33:27 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-12 15:33:27 +0000 |
commit | 9a9a8ab4c2a07aa8faa04f50d6250930220b5be5 (patch) | |
tree | e6cbd9730c892dc6386b9c1c68d53489b478f6f8 /lib/hook.ml | |
parent | 0e69a26eadeabf5987aacdac57cd6a5b90b0cdc8 (diff) |
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
Diffstat (limited to 'lib/hook.ml')
-rw-r--r-- | lib/hook.ml | 32 |
1 files changed, 32 insertions, 0 deletions
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) |