Module Goptions

This module manages customization parameters at the vernacular level

Two kinds of things are managed : tables and options value

Each table/option is uniquely identified by a key of type option_name which consists in a list of strings. Note that for parsing constraints, table names must not be made of more than 2 strings while option names can be of arbitrary length.

The declaration of a table, say of name ["Toto";"Titi"] automatically makes available the following vernacular commands:

Add Toto Titi foo. Remove Toto Titi foo. Print Toto Titi. Test Toto Titi.

The declaration of a non boolean option value, say of name ["Tata";"Tutu";"Titi"], automatically makes available the following vernacular commands:

Set Tata Tutu Titi val. Print Table Tata Tutu Titi.

If it is the declaration of a boolean value, the following vernacular commands are made available:

Set Tata Tutu Titi. Unset Tata Tutu Titi. Print Table Tata Tutu Titi. (** synonym: Test Table Tata Tutu Titi. *)

All options are synchronized with the document.

type option_name = string list
type _ option_kind =
| BoolKind : bool option_kind
| IntKind : int option option_kind
| StringKind : string option_kind
| StringOptKind : string option option_kind
type option_locality =
| OptDefault
| OptLocal
| OptExport
| OptGlobal
Tables.

The functor MakeStringTable declares a table containing objects of type string; the function member_message say what to print when invoking the "Test Toto Titi foo." command; at the end title is the table name printed when invoking the "Print Toto Titi." command; active is roughly the internal version of the vernacular "Test ...": it tells if a given object is in the table; elements returns the list of elements of the table

module MakeStringTable (_ : sig ... end) : sig ... end

The functor MakeRefTable declares a new table of objects of type A.t practically denoted by reference; the encoding function encode : env -> reference -> A.t is typically a globalization function, possibly with some restriction checks; the function member_message say what to print when invoking the "Test Toto Titi foo." command; at the end title is the table name printed when invoking the "Print Toto Titi." command; active is roughly the internal version of the vernacular "Test ...": it tells if a given object is in the table.

module type RefConvertArg = sig ... end
module MakeRefTable (A : RefConvertArg) : sig ... end
Options.

These types and function are for declaring a new option of name key and access functions read and write; the parameter name is the option name used when printing the option value (command "Print Toto Titi."

The declare_*_option functions are low-level, to be used when implementing complex option workflows, e.g. when the option data is in the global env. For most use cases, you should use the helper functions declare_*_option_and_ref.

type 'a option_sig = {
optstage : Summary.Stage.t;
optdepr : Deprecation.t option;(*

whether the option is DEPRECATED

*)
optkey : option_name;(*

the low-level name of this option

*)
optread : unit -> 'a;
optwrite : 'a -> unit;
}
val declare_option : ?preprocess:('a -> 'a) -> kind:'a option_kind -> 'a option_sig -> unit

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.

StringOptKind should be preferred to StringKind because it supports "Unset".

val declare_append_only_option : ?preprocess:(string -> string) -> sep:string -> string option_sig -> unit

Helpers to declare a reference controlled by an option.

type 'a getter = {
get : unit -> 'a;
}

Wrapper type to separate the function calls to register the option at toplevel from the calls to read the option value.

type 'a opt_decl = ?stage:Summary.Stage.t -> ?depr:Deprecation.t -> key:option_name -> value:'a -> unit -> 'a getter
val declare_int_option_and_ref : int opt_decl
val declare_intopt_option_and_ref : int option opt_decl
val declare_nat_option_and_ref : int opt_decl
val declare_bool_option_and_ref : bool opt_decl
val declare_string_option_and_ref : string opt_decl
val declare_stringopt_option_and_ref : string option opt_decl
val declare_interpreted_string_option_and_ref : (string -> 'a) -> ('a -> string) -> 'a opt_decl
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 -> Libobject.locality -> 'a -> unit;
remove : Environ.env -> Libobject.locality -> '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 -> ?stage:Summary.Stage.t -> option_name -> int option -> unit

The first argument is a locality flag. If stage is provided, the option is set/unset only if it is declared in the corresponding stage. If omitted, the option is always set/unset.

val set_bool_option_value_gen : ?locality:option_locality -> ?stage:Summary.Stage.t -> option_name -> bool -> unit
val set_string_option_value_gen : ?locality:option_locality -> ?stage:Summary.Stage.t -> option_name -> string -> unit
val unset_option_value_gen : ?locality:option_locality -> ?stage:Summary.Stage.t -> option_name -> unit
val set_int_option_value : ?stage:Summary.Stage.t -> option_name -> int option -> unit
val set_bool_option_value : ?stage:Summary.Stage.t -> option_name -> bool -> unit
val set_string_option_value : ?stage:Summary.Stage.t -> 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
type table_value =
| StringRefValue of string
| QualidRefValue of Libnames.qualid
val get_option_value : option_name -> (unit -> option_value) option

get_option_value key returns None if option with name key was not found.

type 'a check_and_cast = {
check_and_cast : b. 'a -> 'b option_kind -> 'b;
}
val set_option_value : ?locality:option_locality -> ?stage:Summary.Stage.t -> 'a check_and_cast -> option_name -> 'a -> unit

set_option_value ?locality f name v sets name to the result of applying f to v and name's option kind. Use for behaviour depending on the type of the option, eg erroring when 'a doesn't match it.

type option_state = {
opt_depr : Deprecation.t option;
opt_value : option_value;
}

Summary of an option status

val get_tables : unit -> option_state OptionMap.t
val print_tables : unit -> Pp.t
type iter_table_aux = {
aux : a. 'a table_of_A -> Environ.env -> 'a -> unit;
}
val iter_table : Environ.env -> iter_table_aux -> option_name -> table_value list -> unit
val error_undeclared_key : option_name -> 'a

Compat

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