diff options
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 00000000..0aa373c2 --- /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-2015 *) +(* \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) |