diff options
author | 2017-02-14 18:01:48 +0100 | |
---|---|---|
committer | 2017-02-14 18:21:25 +0100 | |
commit | 3234a893a1b3cfd6b51f1c26cc10e9690d8a703e (patch) | |
tree | 45fdbfc2fd03e30105d1ead1e184bdf6ef822de8 /library | |
parent | cca57bcd89770e76e1bcc21eb41756dca2c51425 (diff) | |
parent | 4fd59386e7f60d16bfe9858c372b354d422ac0b6 (diff) |
Merge branch 'master'.
Diffstat (limited to 'library')
-rw-r--r-- | library/goptions.ml | 11 | ||||
-rw-r--r-- | library/goptions.mli | 14 |
2 files changed, 16 insertions, 9 deletions
diff --git a/library/goptions.ml b/library/goptions.ml index 8f2f06925..1c08b9539 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -247,7 +247,7 @@ let get_locality = function | Some false -> OptGlobal | None -> OptDefault -let declare_option cast uncast append +let declare_option cast uncast append ?(preprocess = fun x -> x) { optsync=sync; optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } = check_key key; let default = read() in @@ -275,10 +275,11 @@ let declare_option cast uncast append subst_function = subst_options; discharge_function = discharge_options; classify_function = classify_options } in - (fun l m v -> Lib.add_anonymous_leaf (options (l, m, v))) + (fun l m v -> let v = preprocess v in Lib.add_anonymous_leaf (options (l, m, v))) else (fun _ m v -> - match m with + let v = preprocess v in + match m with | OptSet -> write v | OptAppend -> write (append (read ()) v)) in @@ -381,9 +382,9 @@ let msg_option_value (name,v) = | BoolValue false -> str "off" | IntValue (Some n) -> int n | IntValue None -> str "undefined" - | StringValue s -> str s + | StringValue s -> quote (str s) | StringOptValue None -> str"undefined" - | StringOptValue (Some s) -> str s + | StringOptValue (Some s) -> quote (str s) (* | IdentValue r -> pr_global_env Id.Set.empty r *) let print_option_value key = diff --git a/library/goptions.mli b/library/goptions.mli index ca2df0710..3b3651f39 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -122,13 +122,19 @@ type 'a option_sig = { (** When an option is declared synchronous ([optsync] is [true]), the output is a synchronous write function. Otherwise it is [optwrite] *) +(** The [preprocess] function is triggered before setting the option. It can be + used to emit a warning on certain values, and clean-up the final value. *) type 'a write_function = 'a -> unit -val declare_int_option : int option option_sig -> int option write_function -val declare_bool_option : bool option_sig -> bool write_function -val declare_string_option: string option_sig -> string write_function -val declare_stringopt_option: string option option_sig -> string option write_function +val declare_int_option : ?preprocess:(int option -> int option) -> + int option option_sig -> int option write_function +val declare_bool_option : ?preprocess:(bool -> bool) -> + bool option_sig -> bool write_function +val declare_string_option: ?preprocess:(string -> string) -> + string option_sig -> string write_function +val declare_stringopt_option: ?preprocess:(string option -> string option) -> + string option option_sig -> string option write_function (** {6 Special functions supposed to be used only in vernacentries.ml } *) |