diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-02-28 13:45:04 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-03-09 10:17:21 -0300 |
commit | 25b07a6f824654be2041152d904507bc62102986 (patch) | |
tree | 82f9d96e40911f85347ed4e5bc273cc6a15627f9 /library/goptions.ml | |
parent | 38a671f74857aec8e285a6a0bfcab876e3b9a133 (diff) |
Implement the Export Set/Unset feature.
This feature has been asked many times by different people, and allows to
have options in a module that are performed when this module is imported.
This supersedes the well-numbered cursed PR #313.
Diffstat (limited to 'library/goptions.ml')
-rw-r--r-- | library/goptions.ml | 22 |
1 files changed, 18 insertions, 4 deletions
diff --git a/library/goptions.ml b/library/goptions.ml index 5cd82e56f..76071ebcc 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -196,7 +196,7 @@ type 'a option_sig = { optread : unit -> 'a; optwrite : 'a -> unit } -type option_locality = OptLocal | OptDefault | OptGlobal +type option_locality = OptDefault | OptLocal | OptExport | OptGlobal type option_mod = OptSet | OptAppend @@ -242,16 +242,30 @@ let declare_option cast uncast append ?(preprocess = fun x -> x) match m with | OptSet -> write v | OptAppend -> write (append (read ()) v) in - let load_options i o = cache_options o in + let load_options i (_, (l, _, _) as o) = match l with + | OptGlobal -> cache_options o + | OptExport -> () + | OptLocal | OptDefault -> + (** Ruled out by classify_function *) + assert false + in + let open_options i (_, (l, _, _) as o) = match l with + | OptExport -> if Int.equal i 1 then cache_options o + | OptGlobal -> () + | OptLocal | OptDefault -> + (** Ruled out by classify_function *) + assert false + in let subst_options (subst,obj) = obj in let discharge_options (_,(l,_,_ as o)) = - match l with OptLocal -> None | (OptGlobal | OptDefault) -> Some o in + match l with OptLocal -> None | (OptExport | OptGlobal | OptDefault) -> Some o in let classify_options (l,_,_ as o) = - match l with OptGlobal -> Substitute o | (OptLocal | OptDefault) -> Dispose in + match l with (OptExport | OptGlobal) -> Substitute o | (OptLocal | OptDefault) -> Dispose in let options : option_locality * option_mod * _ -> obj = declare_object { (default_object (nickname key)) with load_function = load_options; + open_function = open_options; cache_function = cache_options; subst_function = subst_options; discharge_function = discharge_options; |