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

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