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_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 setting one option changes the value of another. 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;
}

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.

declare_stringopt_option should be preferred to declare_string_option because it supports "Unset". Only "Warnings" option is declared using the latter.

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

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 set_string_option_append_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.

val set_option_value : ?locality:option_locality -> ?stage:Summary.Stage.t -> ('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 : 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