aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-01-27 02:56:03 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-01-30 19:29:17 +0100
commit779c0bd23bbc0bd1d0c1cb358fe9725e7d7ccc74 (patch)
tree213309c2c8da155bb4e28e8f668129781e6b5baa /lib
parent879ebad4d0b39fda275a72ba44c1f4dfbb9282e5 (diff)
[lib] Respect change of options under with/without_option.
The old semantics of `with/without_option` allowed the called function to modify the value of the option. This is an issue mainly with the `silently/verbose` combinators, as `Set Silent` can be executed under one of them and thus the modification will be lost in the updated code introduced in a554519874c15d0a790082e5f15f3dc2419c6c38 IMHO these kind of semantics are quite messy but we have to preserve them in order for the `Silent` system to work. In fact, note that in the previous code, `with_options` was not consistent with `with_option` [maybe that got me confused?] Ideally we could restore the saner semantics once we clean up the `Silent` system [that is, we remove the flag altogether], but that'll have to wait. Fixes #6645.
Diffstat (limited to 'lib')
-rw-r--r--lib/flags.ml18
1 files changed, 14 insertions, 4 deletions
diff --git a/lib/flags.ml b/lib/flags.ml
index ee4c0734a..01361dad5 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -6,18 +6,28 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-let with_modified_ref r nf f x =
+(* If [restore] is false, whenever [f] modifies the ref, we will
+ preserve the modification. *)
+let with_modified_ref ?(restore=true) r nf f x =
let old_ref = !r in r := nf !r;
- try let res = f x in r := old_ref; res
+ try
+ let pre = !r in
+ let res = f x in
+ (* If r was modified don't restore its old value *)
+ if restore || pre == !r then r := old_ref;
+ res
with reraise ->
let reraise = Backtrace.add_backtrace reraise in
r := old_ref;
Exninfo.iraise reraise
-let with_option o f x = with_modified_ref o (fun _ -> true) f x
-let without_option o f x = with_modified_ref o (fun _ -> false) f x
+let with_option o f x = with_modified_ref ~restore:false o (fun _ -> true) f x
+let without_option o f x = with_modified_ref ~restore:false o (fun _ -> false) f x
let with_extra_values o l f x = with_modified_ref o (fun ol -> ol@l) f x
+(* hide the [restore] option as internal *)
+let with_modified_ref r nf f x = with_modified_ref r nf f x
+
let with_options ol f x =
let vl = List.map (!) ol in
let () = List.iter (fun r -> r := true) ol in