diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 1 | ||||
| -rw-r--r-- | library/global.mli | 1 | ||||
| -rw-r--r-- | library/goptions.ml | 20 | ||||
| -rw-r--r-- | library/goptions.mli | 13 |
4 files changed, 22 insertions, 13 deletions
diff --git a/library/global.ml b/library/global.ml index 4ea5969a6f..67b00cf411 100644 --- a/library/global.ml +++ b/library/global.ml @@ -88,6 +88,7 @@ let add_constraints c = globalize0 (Safe_typing.add_constraints c) let push_context_set b c = globalize0 (Safe_typing.push_context_set b c) let set_engagement c = globalize0 (Safe_typing.set_engagement c) +let set_indices_matter b = globalize0 (Safe_typing.set_indices_matter b) let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c) let typing_flags () = Environ.typing_flags (env ()) let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd) diff --git a/library/global.mli b/library/global.mli index 01ee695c49..40962e21af 100644 --- a/library/global.mli +++ b/library/global.mli @@ -29,6 +29,7 @@ val named_context : unit -> Constr.named_context (** Changing the (im)predicativity of the system *) val set_engagement : Declarations.engagement -> unit +val set_indices_matter : bool -> unit val set_typing_flags : Declarations.typing_flags -> unit val typing_flags : unit -> Declarations.typing_flags diff --git a/library/goptions.ml b/library/goptions.ml index 154b863fa1..98efb512ab 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -276,10 +276,7 @@ let declare_option cast uncast append ?(preprocess = fun x -> x) 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, (cread,cwrite,cappend)) !value_tab; - write - -type 'a write_function = 'a -> unit + value_tab := OptionMap.add key (name, depr, (cread,cwrite,cappend)) !value_tab let declare_int_option = declare_option @@ -302,6 +299,18 @@ let declare_stringopt_option = (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option.")) (fun _ _ -> anomaly (Pp.str "async_option.")) +let declare_bool_option_and_ref ~depr ~name ~key ~(value:bool) = + let r_opt = ref value in + let optwrite v = r_opt := v in + let optread () = !r_opt in + let _ = declare_bool_option { + optdepr = depr; + optname = name; + optkey = key; + optread; optwrite + } in + optread + (* 3- User accessible commands *) (* Setting values of options *) @@ -425,6 +434,3 @@ let print_tables () = (fun (nickkey,_) p -> p ++ str " " ++ str nickkey ++ fnl ()) !ref_table (mt ()) ++ fnl () - - - diff --git a/library/goptions.mli b/library/goptions.mli index 3d7df18fed..b91553bf3c 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -122,17 +122,18 @@ type 'a option_sig = { (** The [preprocess] function is triggered before setting the option. It can be used to emit a warning on certain values, and clean-up the final value. *) -type 'a write_function = 'a -> unit - val declare_int_option : ?preprocess:(int option -> int option) -> - int option option_sig -> int option write_function + int option option_sig -> unit val declare_bool_option : ?preprocess:(bool -> bool) -> - bool option_sig -> bool write_function + bool option_sig -> unit val declare_string_option: ?preprocess:(string -> string) -> - string option_sig -> string write_function + string option_sig -> unit val declare_stringopt_option: ?preprocess:(string option -> string option) -> - string option option_sig -> string option write_function + string option option_sig -> unit +(** Helper to declare a reference controlled by an option. Read-only + as to avoid races. *) +val declare_bool_option_and_ref : depr:bool -> name:string -> key:option_name -> value:bool -> (unit -> bool) (** {6 Special functions supposed to be used only in vernacentries.ml } *) |