From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- library/goptions.ml | 155 +++++++++++++++++++++++----------------------------- 1 file changed, 68 insertions(+), 87 deletions(-) (limited to 'library/goptions.ml') diff --git a/library/goptions.ml b/library/goptions.ml index 9dc0f405..eb7bb5b4 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* t val subst : substitution -> t -> t - val printer : t -> std_ppcmds + val printer : t -> Pp.t val key : option_name val title : string - val member_message : t -> bool -> std_ppcmds - val synchronous : bool + val member_message : t -> bool -> Pp.t end) -> struct type option_mark = @@ -73,17 +73,13 @@ module MakeTable = let _ = if String.List.mem_assoc nick !A.table then - error "Sorry, this table name is already used." + user_err Pp.(str "Sorry, this table name is already used.") module MySet = Set.Make (struct type t = A.t let compare = A.compare end) - let t = - if A.synchronous - then Summary.ref MySet.empty ~name:nick - else ref MySet.empty + let t = Summary.ref MySet.empty ~name:nick 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 @@ -103,9 +99,6 @@ module MakeTable = in ((fun c -> Lib.add_anonymous_leaf (inGo (GOadd, c))), (fun c -> Lib.add_anonymous_leaf (inGo (GOrmv, c)))) - else - ((fun c -> t := MySet.add c !t), - (fun c -> t := MySet.remove c !t)) let print_table table_name printer table = Feedback.msg_notice @@ -140,8 +133,7 @@ module type StringConvertArg = sig val key : option_name val title : string - val member_message : string -> bool -> std_ppcmds - val synchronous : bool + val member_message : string -> bool -> Pp.t end module StringConvert = functor (A : StringConvertArg) -> @@ -156,7 +148,6 @@ struct let key = A.key let title = A.title let member_message = A.member_message - let synchronous = A.synchronous end module MakeStringTable = @@ -172,11 +163,10 @@ sig val compare : t -> t -> int val encode : reference -> t val subst : substitution -> t -> t - val printer : t -> std_ppcmds + val printer : t -> Pp.t val key : option_name val title : string - val member_message : t -> bool -> std_ppcmds - val synchronous : bool + val member_message : t -> bool -> Pp.t end module RefConvert = functor (A : RefConvertArg) -> @@ -191,7 +181,6 @@ struct let key = A.key let title = A.title let member_message = A.member_message - let synchronous = A.synchronous end module MakeRefTable = @@ -201,14 +190,13 @@ module MakeRefTable = (* 2- Flags. *) type 'a option_sig = { - optsync : bool; optdepr : bool; optname : string; optkey : option_name; optread : unit -> 'a; optwrite : 'a -> unit } -type option_locality = OptLocal | OptDefault | OptGlobal +type option_locality = OptDefault | OptLocal | OptExport | OptGlobal type option_mod = OptSet | OptAppend @@ -228,31 +216,24 @@ let get_option key = OptionMap.find key !value_tab let check_key key = try let _ = get_option key in - error "Sorry, this option name is already used." + user_err Pp.(str "Sorry, this option name is already used.") with Not_found -> 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." + then user_err Pp.(str "Sorry, this option name is already used.") open Libobject -open Lib let warn_deprecated_option = CWarnings.create ~name:"deprecated-option" ~category:"deprecated" (fun key -> str "Option" ++ spc () ++ str (nickname key) ++ strbrk " is deprecated") -let get_locality = function - | Some true -> OptLocal - | Some false -> OptGlobal - | None -> OptDefault - let declare_option cast uncast append ?(preprocess = fun x -> x) - { optsync=sync; optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } = + { optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } = check_key key; let default = read() in let change = - if sync then let _ = Summary.declare_summary (nickname key) { Summary.freeze_function = (fun _ -> read ()); Summary.unfreeze_function = write; @@ -261,33 +242,41 @@ let declare_option cast uncast append ?(preprocess = fun x -> x) match m with | OptSet -> write v | OptAppend -> write (append (read ()) v) in - let load_options i o = cache_options o in + let load_options i (_, (l, _, _) as o) = match l with + | OptGlobal -> cache_options o + | OptExport -> () + | OptLocal | OptDefault -> + (** Ruled out by classify_function *) + assert false + in + let open_options i (_, (l, _, _) as o) = match l with + | OptExport -> if Int.equal i 1 then cache_options o + | OptGlobal -> () + | OptLocal | OptDefault -> + (** Ruled out by classify_function *) + assert false + in let subst_options (subst,obj) = obj in let discharge_options (_,(l,_,_ as o)) = - match l with OptLocal -> None | _ -> Some o in + match l with OptLocal -> None | (OptExport | OptGlobal | OptDefault) -> Some o in let classify_options (l,_,_ as o) = - match l with OptGlobal -> Substitute o | _ -> Dispose in + match l with (OptExport | OptGlobal) -> Substitute o | (OptLocal | OptDefault) -> Dispose in let options : option_locality * option_mod * _ -> obj = declare_object { (default_object (nickname key)) with load_function = load_options; + open_function = open_options; cache_function = cache_options; subst_function = subst_options; discharge_function = discharge_options; classify_function = classify_options } in (fun l m v -> let v = preprocess v in Lib.add_anonymous_leaf (options (l, m, v))) - else - (fun _ m v -> - let v = preprocess v in - match m with - | OptSet -> write v - | OptAppend -> write (append (read ()) v)) in let warn () = if depr then warn_deprecated_option key in let cread () = cast (read ()) in let cwrite l v = warn (); change l OptSet (uncast v) in let cappend l v = warn (); change l OptAppend (uncast v) in - value_tab := OptionMap.add key (name, depr, (sync,cread,cwrite,cappend)) !value_tab; + value_tab := OptionMap.add key (name, depr, (cread,cwrite,cappend)) !value_tab; write type 'a write_function = 'a -> unit @@ -295,23 +284,23 @@ type 'a write_function = 'a -> unit let declare_int_option = declare_option (fun v -> IntValue v) - (function IntValue v -> v | _ -> anomaly (Pp.str "async_option")) - (fun _ _ -> anomaly (Pp.str "async_option")) + (function IntValue v -> v | _ -> anomaly (Pp.str "async_option.")) + (fun _ _ -> anomaly (Pp.str "async_option.")) let declare_bool_option = declare_option (fun v -> BoolValue v) - (function BoolValue v -> v | _ -> anomaly (Pp.str "async_option")) - (fun _ _ -> anomaly (Pp.str "async_option")) + (function BoolValue v -> v | _ -> anomaly (Pp.str "async_option.")) + (fun _ _ -> anomaly (Pp.str "async_option.")) let declare_string_option = declare_option (fun v -> StringValue v) - (function StringValue v -> v | _ -> anomaly (Pp.str "async_option")) + (function StringValue v -> v | _ -> anomaly (Pp.str "async_option.")) (fun x y -> x^","^y) let declare_stringopt_option = declare_option (fun v -> StringOptValue v) - (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option")) - (fun _ _ -> anomaly (Pp.str "async_option")) + (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option.")) + (fun _ _ -> anomaly (Pp.str "async_option.")) (* 3- User accessible commands *) @@ -322,14 +311,14 @@ let warn_unknown_option = (fun key -> strbrk "There is no option " ++ str (nickname key) ++ str ".") -let set_option_value locality check_and_cast key v = +let set_option_value ?(locality = OptDefault) check_and_cast key v = let opt = try Some (get_option key) with Not_found -> None in match opt with | None -> warn_unknown_option key - | Some (name, depr, (_,read,write,append)) -> - write (get_locality locality) (check_and_cast v (read ())) + | Some (name, depr, (read,write,append)) -> + write locality (check_and_cast v (read ())) -let bad_type_error () = error "Bad type of value for this option." +let bad_type_error () = user_err Pp.(str "Bad type of value for this option.") let check_int_value v = function | IntValue _ -> IntValue v @@ -354,25 +343,25 @@ let check_unset_value v = function warning. This allows a script to refer to an option that doesn't exist anymore *) -let set_int_option_value_gen locality = - set_option_value locality check_int_value -let set_bool_option_value_gen locality key v = - set_option_value locality check_bool_value key v -let set_string_option_value_gen locality = - set_option_value locality check_string_value -let unset_option_value_gen locality key = - set_option_value locality check_unset_value key () +let set_int_option_value_gen ?locality = + set_option_value ?locality check_int_value +let set_bool_option_value_gen ?locality key v = + set_option_value ?locality check_bool_value key v +let set_string_option_value_gen ?locality = + set_option_value ?locality check_string_value +let unset_option_value_gen ?locality key = + set_option_value ?locality check_unset_value key () -let set_string_option_append_value_gen locality key v = +let set_string_option_append_value_gen ?(locality = OptDefault) key v = let opt = try Some (get_option key) with Not_found -> None in match opt with | None -> warn_unknown_option key - | Some (name, depr, (_,read,write,append)) -> - append (get_locality locality) (check_string_value v (read ())) + | Some (name, depr, (read,write,append)) -> + append locality (check_string_value v (read ())) -let set_int_option_value = set_int_option_value_gen None -let set_bool_option_value = set_bool_option_value_gen None -let set_string_option_value = set_string_option_value_gen None +let set_int_option_value opt v = set_int_option_value_gen opt v +let set_bool_option_value opt v = set_bool_option_value_gen opt v +let set_string_option_value opt v = set_string_option_value_gen opt v (* Printing options/tables *) @@ -382,13 +371,13 @@ let msg_option_value (name,v) = | BoolValue false -> str "off" | IntValue (Some n) -> int n | IntValue None -> str "undefined" - | StringValue s -> str "\"" ++ str s ++ str "\"" + | StringValue s -> quote (str s) | StringOptValue None -> str"undefined" - | StringOptValue (Some s) -> str "\"" ++ str s ++ str "\"" + | StringOptValue (Some s) -> quote (str s) (* | IdentValue r -> pr_global_env Id.Set.empty r *) let print_option_value key = - let (name, depr, (_,read,_,_)) = get_option key in + let (name, depr, (read,_,_)) = get_option key in let s = read () in match s with | BoolValue b -> @@ -398,9 +387,8 @@ let print_option_value key = let get_tables () = let tables = !value_tab in - let fold key (name, depr, (sync,read,_,_)) accu = + let fold key (name, depr, (read,_,_)) accu = let state = { - opt_sync = sync; opt_name = name; opt_depr = depr; opt_value = read (); @@ -415,17 +403,10 @@ let print_tables () = if depr then msg ++ str " [DEPRECATED]" ++ fnl () else msg ++ fnl () in - 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 () ++ + str "Options:" ++ fnl () ++ OptionMap.fold - (fun key (name, depr, (sync,read,_,_)) p -> - if sync then p - else p ++ print_option key name (read ()) depr) + (fun key (name, depr, (read,_,_)) p -> + p ++ print_option key name (read ()) depr) !value_tab (mt ()) ++ str "Tables:" ++ fnl () ++ List.fold_right -- cgit v1.2.3