Module Goptions

This module manages customization parameters at the vernacular level

type option_name = string list
type option_locality =
| OptDefault
| OptLocal
| OptExport
| OptGlobal
Tables.
module MakeStringTable : functor (A : sig ... end) -> sig ... end
module MakeRefTable : functor (A : sig ... end) -> sig ... end
Options.
type 'a option_sig = {
optdepr : bool;

whether the option is DEPRECATED

optname : string;

a short string describing the option

optkey : option_name;

the low-level name of this option

optread : unit -> 'a;
optwrite : 'a -> unit;
}
val declare_int_option : ?⁠preprocess:(int option -> int option) -> int option option_sig -> unit
val declare_bool_option : ?⁠preprocess:(bool -> bool) -> bool option_sig -> unit
val declare_string_option : ?⁠preprocess:(string -> string) -> string option_sig -> unit
val declare_stringopt_option : ?⁠preprocess:(string option -> string option) -> string option option_sig -> unit
val declare_bool_option_and_ref : depr:bool -> name:string -> key:option_name -> value:bool -> unit -> bool

Helper to declare a reference controlled by an option. Read-only as to avoid races.

Special functions supposed to be used only in vernacentries.ml
module OptionMap : CSig.MapS with type key = option_name
type 'a table_of_A = {
add : Environ.env -> 'a -> unit;
remove : Environ.env -> 'a -> unit;
mem : Environ.env -> 'a -> unit;
print : unit -> unit;
}
val get_string_table : option_name -> string table_of_A
val get_ref_table : option_name -> Libnames.qualid table_of_A
val set_int_option_value_gen : ?⁠locality:option_locality -> option_name -> int option -> unit

The first argument is a locality flag.

val set_bool_option_value_gen : ?⁠locality:option_locality -> option_name -> bool -> unit
val set_string_option_value_gen : ?⁠locality:option_locality -> option_name -> string -> unit
val set_string_option_append_value_gen : ?⁠locality:option_locality -> option_name -> string -> unit
val unset_option_value_gen : ?⁠locality:option_locality -> option_name -> unit
val set_int_option_value : option_name -> int option -> unit
val set_bool_option_value : option_name -> bool -> unit
val set_string_option_value : option_name -> string -> unit
val print_option_value : option_name -> unit
type option_value =
| BoolValue of bool
| IntValue of int option
| StringValue of string
| StringOptValue of string option
val set_option_value : ?⁠locality:option_locality -> ('a -> option_value -> option_value) -> option_name -> 'a -> unit

set_option_value ?locality f name v sets name to the result of applying f to v and name's current value. Use for behaviour depending on the type of the option, eg erroring when 'a doesn't match it. Changing the type will result in errors later so don't do that.

type option_state = {
opt_depr : bool;
opt_name : string;
opt_value : option_value;
}

Summary of an option status

val get_tables : unit -> option_state OptionMap.t
val print_tables : unit -> Pp.t
val error_undeclared_key : option_name -> 'a