diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-11-03 17:55:37 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-11-03 17:55:37 +0100 |
| commit | 0c01a177362f8d7408ba8906fe0cba1948d8fb9c (patch) | |
| tree | ee84a305e691da2d6c87eb830c4b94376f2f19e1 /library/goptions.ml | |
| parent | df1720bff67889818f8b4856f29ac02540d7f756 (diff) | |
| parent | 2c5eef988f11979175de6d1983bc533ce18b1095 (diff) | |
Merge remote-tracking branch 'github/pr/340' into v8.6
Was PR#340: Fix various shortcomings of the warnings infrastructure.
Diffstat (limited to 'library/goptions.ml')
| -rw-r--r-- | library/goptions.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/library/goptions.ml b/library/goptions.ml index 35616558a..9dc0f4058 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 -> str "\"" ++ str s ++ str "\"" | StringOptValue None -> str"undefined" - | StringOptValue (Some s) -> str s + | StringOptValue (Some s) -> str "\"" ++ str s ++ str "\"" (* | IdentValue r -> pr_global_env Id.Set.empty r *) let print_option_value key = |