From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- library/goptions.ml | 143 +++++++++++++++++++++++++++------------------------- 1 file changed, 73 insertions(+), 70 deletions(-) (limited to 'library/goptions.ml') diff --git a/library/goptions.ml b/library/goptions.ml index d92fe262..4aea3368 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* t -> int val table : (string * key table_of_A) list ref val encode : key -> t val subst : substitution -> t -> t @@ -62,29 +71,22 @@ module MakeTable = let nick = nickname A.key let _ = - if List.mem_assoc nick !A.table then + if String.List.mem_assoc nick !A.table then error "Sorry, this table name is already used." - module MySet = Set.Make (struct type t = A.t let compare = compare end) + module MySet = Set.Make (struct type t = A.t let compare = A.compare end) - let t = ref (MySet.empty : MySet.t) - - let _ = - if A.synchronous then - let freeze () = !t in - let unfreeze c = t := c in - let init () = t := MySet.empty in - Summary.declare_summary nick - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init } + let t = + if A.synchronous + then Summary.ref MySet.empty ~name:nick + else ref MySet.empty let (add_option,remove_option) = if A.synchronous then let cache_options (_,(f,p)) = match f with | GOadd -> t := MySet.add p !t | GOrmv -> t := MySet.remove p !t in - let load_options i o = if i=1 then cache_options o in + let load_options i o = if Int.equal i 1 then cache_options o in let subst_options (subst,(f,p as obj)) = let p' = A.subst subst p in if p' == p then obj else @@ -105,12 +107,12 @@ module MakeTable = (fun c -> t := MySet.remove c !t)) let print_table table_name printer table = - msg (str table_name ++ + pp (str table_name ++ (hov 0 - (if MySet.is_empty table then str "None" ++ fnl () + (if MySet.is_empty table then str " None" ++ fnl () else MySet.fold - (fun a b -> printer a ++ spc () ++ b) - table (mt ()) ++ fnl ()))) + (fun a b -> spc () ++ printer a ++ b) + table (mt ()) ++ str "." ++ fnl ()))) class table_of_A () = object @@ -119,7 +121,7 @@ module MakeTable = method mem x = let y = A.encode x in let answer = MySet.mem y !t in - msg (A.member_message y answer ++ fnl ()) + msg_info (A.member_message y answer) method print = print_table A.title A.printer !t end @@ -130,7 +132,7 @@ module MakeTable = let string_table = ref [] -let get_string_table k = List.assoc (nickname k) !string_table +let get_string_table k = String.List.assoc (nickname k) !string_table module type StringConvertArg = sig @@ -144,6 +146,7 @@ module StringConvert = functor (A : StringConvertArg) -> struct type t = string type key = string + let compare = String.compare let table = string_table let encode x = x let subst _ x = x @@ -159,11 +162,12 @@ module MakeStringTable = let ref_table = ref [] -let get_ref_table k = List.assoc (nickname k) !ref_table +let get_ref_table k = String.List.assoc (nickname k) !ref_table module type RefConvertArg = sig type t + val compare : t -> t -> int val encode : reference -> t val subst : substitution -> t -> t val printer : t -> std_ppcmds @@ -177,6 +181,7 @@ module RefConvert = functor (A : RefConvertArg) -> struct type t = A.t type key = reference + let compare = A.compare let table = ref_table let encode = A.encode let subst = A.subst @@ -201,10 +206,13 @@ type 'a option_sig = { optread : unit -> 'a; optwrite : 'a -> unit } -type option_type = bool * (unit -> option_value) -> (option_value -> unit) +module OptionOrd = +struct + type t = option_name + let compare opt1 opt2 = List.compare String.compare opt1 opt2 +end -module OptionMap = - Map.Make (struct type t = option_name let compare = compare end) +module OptionMap = Map.Make(OptionOrd) let value_tab = ref OptionMap.empty @@ -216,11 +224,10 @@ let check_key key = try let _ = get_option key in error "Sorry, this option name is already used." with Not_found -> - if List.mem_assoc (nickname key) !string_table - or List.mem_assoc (nickname key) !ref_table + if String.List.mem_assoc (nickname key) !string_table + || String.List.mem_assoc (nickname key) !ref_table then error "Sorry, this option name is already used." -open Summary open Libobject open Lib @@ -251,10 +258,10 @@ let declare_option cast uncast discharge_function = (fun (_,v) -> Some v); load_function = (fun _ (_,v) -> write v)} in - let _ = declare_summary (nickname key) - { freeze_function = read; - unfreeze_function = write; - init_function = (fun () -> write default) } + let _ = Summary.declare_summary (nickname key) + { Summary.freeze_function = (fun _ -> read ()); + Summary.unfreeze_function = write; + Summary.init_function = (fun () -> write default) } in begin fun v -> add_anonymous_leaf (decl_obj v) end , begin fun v -> add_anonymous_leaf (ldecl_obj v) end , @@ -273,15 +280,15 @@ type 'a write_function = 'a -> unit let declare_int_option = declare_option (fun v -> IntValue v) - (function IntValue v -> v | _ -> anomaly "async_option") + (function IntValue v -> v | _ -> anomaly (Pp.str "async_option")) let declare_bool_option = declare_option (fun v -> BoolValue v) - (function BoolValue v -> v | _ -> anomaly "async_option") + (function BoolValue v -> v | _ -> anomaly (Pp.str "async_option")) let declare_string_option = declare_option (fun v -> StringValue v) - (function StringValue v -> v | _ -> anomaly "async_option") + (function StringValue v -> v | _ -> anomaly (Pp.str "async_option")) (* 3- User accessible commands *) @@ -326,12 +333,12 @@ let set_int_option_value_gen locality = set_option_value locality check_int_value let set_bool_option_value_gen locality key v = try set_option_value locality check_bool_value key v - with UserError (_,s) -> Flags.if_warn msg_warning s + with UserError (_,s) -> msg_warning s let set_string_option_value_gen locality = set_option_value locality check_string_value let unset_option_value_gen locality key = try set_option_value locality check_unset_value key () - with UserError (_,s) -> Flags.if_warn msg_warning s + with UserError (_,s) -> msg_warning s let set_int_option_value = set_int_option_value_gen None let set_bool_option_value = set_bool_option_value_gen None @@ -346,19 +353,16 @@ let msg_option_value (name,v) = | IntValue (Some n) -> int n | IntValue None -> str "undefined" | StringValue s -> str s -(* | IdentValue r -> pr_global_env Idset.empty r *) +(* | IdentValue r -> pr_global_env Id.Set.empty r *) let print_option_value key = let (name, depr, (_,read,_,_,_)) = get_option key in let s = read () in match s with | BoolValue b -> - msg (str ("The "^name^" mode is "^(if b then "on" else "off")) ++ - fnl ()) + msg_info (str ("The "^name^" mode is "^(if b then "on" else "off"))) | _ -> - msg (str ("Current value of "^name^" is ") ++ - msg_option_value (name,s) ++ fnl ()) - + msg_info (str ("Current value of "^name^" is ") ++ msg_option_value (name, s)) let get_tables () = let tables = !value_tab in @@ -379,27 +383,26 @@ let print_tables () = if depr then msg ++ str " [DEPRECATED]" ++ fnl () else msg ++ fnl () in - msg - (str "Synchronous options:" ++ fnl () ++ - OptionMap.fold - (fun key (name, depr, (sync,read,_,_,_)) p -> - if sync then p ++ print_option key name (read ()) depr - else p) - !value_tab (mt ()) ++ - str "Asynchronous options:" ++ fnl () ++ - OptionMap.fold - (fun key (name, depr, (sync,read,_,_,_)) p -> - if sync then p - else p ++ print_option key name (read ()) depr) - !value_tab (mt ()) ++ - str "Tables:" ++ fnl () ++ - List.fold_right - (fun (nickkey,_) p -> p ++ str (" "^nickkey) ++ fnl ()) - !string_table (mt ()) ++ - List.fold_right - (fun (nickkey,_) p -> p ++ str (" "^nickkey) ++ fnl ()) - !ref_table (mt ()) ++ - fnl () - ) + str "Synchronous options:" ++ fnl () ++ + OptionMap.fold + (fun key (name, depr, (sync,read,_,_,_)) p -> + if sync then p ++ print_option key name (read ()) depr + else p) + !value_tab (mt ()) ++ + str "Asynchronous options:" ++ fnl () ++ + OptionMap.fold + (fun key (name, depr, (sync,read,_,_,_)) p -> + if sync then p + else p ++ print_option key name (read ()) depr) + !value_tab (mt ()) ++ + str "Tables:" ++ fnl () ++ + List.fold_right + (fun (nickkey,_) p -> p ++ str (" "^nickkey) ++ fnl ()) + !string_table (mt ()) ++ + List.fold_right + (fun (nickkey,_) p -> p ++ str (" "^nickkey) ++ fnl ()) + !ref_table (mt ()) ++ + fnl () + -- cgit v1.2.3