diff options
| author | letouzey | 2001-10-24 06:50:03 +0000 |
|---|---|---|
| committer | letouzey | 2001-10-24 06:50:03 +0000 |
| commit | 53b680024f0f4d68796cdcacc162b57409a1ca14 (patch) | |
| tree | 975c015c014608669dbb52c0de3f1e069e741c24 /library | |
| parent | 69bf012d0d2a71ed19fc89b31073747f85f9a11d (diff) | |
Patch de goption.ml pour faire marcher les options synchrones. Passage des options d'extraction en synchrone
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2137 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
| -rw-r--r-- | library/goptions.ml | 5 |
1 files changed, 4 insertions, 1 deletions
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 |