diff options
| -rw-r--r-- | contrib/extraction/table.ml | 26 | ||||
| -rw-r--r-- | library/goptions.ml | 5 |
2 files changed, 12 insertions, 19 deletions
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index bca08db34e..b798d13e43 100644 --- a/contrib/extraction/table.ml +++ b/contrib/extraction/table.ml @@ -53,31 +53,21 @@ let refs_of_vargl = List.map reference_of_varg (*s AutoInline parameter *) -let auto_inline_ref = ref true - -let auto_inline () = !auto_inline_ref - let auto_inline_params = - {optasyncname = "Extraction AutoInline"; - optasynckey = SecondaryTable ("Extraction", "AutoInline"); - optasyncread = auto_inline; - optasyncwrite = (fun b ->auto_inline_ref := b)} + {optsyncname = "Extraction AutoInline"; + optsynckey = SecondaryTable ("Extraction", "AutoInline"); + optsyncdefault = true } -let _ = declare_async_bool_option auto_inline_params +let auto_inline = declare_sync_bool_option auto_inline_params (*s Optimize parameter *) -let optim_ref = ref true - -let optim () = !optim_ref - let optim_params = - {optasyncname = "Extraction Optimize"; - optasynckey = SecondaryTable ("Extraction", "Optimize"); - optasyncread = optim; - optasyncwrite = (fun b ->optim_ref := b)} + {optsyncname = "Extraction Optimize"; + optsynckey = SecondaryTable ("Extraction", "Optimize"); + optsyncdefault = true } -let _ = declare_async_bool_option optim_params +let optim = declare_sync_bool_option optim_params (*s Table for custom inlining *) diff --git a/library/goptions.ml b/library/goptions.ml index 94fb126681..77ce794ce2 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -205,6 +205,7 @@ type option_value_ref = module Key = struct type t = option_name let compare = Pervasives.compare end module OptionMap = Map.Make(Key) +let sync_value_init_tab = ref OptionMap.empty let sync_value_tab = ref OptionMap.empty let async_value_tab = ref OptionMap.empty @@ -224,7 +225,7 @@ let (inOptVal,_) = let freeze_sync_table () = !sync_value_tab let unfreeze_sync_table l = sync_value_tab := l -let init_sync_table () = sync_value_tab := OptionMap.empty +let init_sync_table () = sync_value_tab := !sync_value_init_tab let _ = Summary.declare_summary "Sync_option" { Summary.freeze_function = freeze_sync_table; @@ -263,6 +264,8 @@ let declare_sync_option (cast,uncast) or List.mem_assoc (nickname key) !ident_table then error "Sorry, this option name is already used"; sync_value_tab := OptionMap.add key (name,(cast default)) !sync_value_tab; + sync_value_init_tab := + OptionMap.add key (name,(cast default)) !sync_value_init_tab; fun () -> uncast (snd (OptionMap.find key !sync_value_tab)) type 'a value_function = unit -> 'a |