Module `Goptions`Source

This module manages customization parameters at the vernacular level

Two kinds of things are managed : tables and options value

Tables are created by applying the MakeTable functor.
Variables storing options value are created by applying one of the declare_int_option, declare_bool_option, ... functions.

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.

Sourcetype option_name = string list

Sourcetype 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

Sourcemodule MakeStringTable (A : 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.

Sourcemodule MakeRefTable (A : sig ... end) : 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.

Sourcetype 'a option_sig = {

optdepr : bool;
(*
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.

Source

val declare_int_option : 
  ?preprocess:(int option -> int option) ->
  int option option_sig ->
  unit

Sourceval declare_bool_option : ?preprocess:(bool -> bool) -> bool option_sig -> unit

Source

val declare_string_option : 
  ?preprocess:(string -> string) ->
  string option_sig ->
  unit

Source

val declare_stringopt_option : 
  ?preprocess:(string option -> string option) ->
  string option option_sig ->
  unit

Sourcetype 'a opt_decl = depr:bool -> key:option_name -> 'a

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

Sourceval declare_int_option_and_ref : (value:int -> unit -> int) opt_decl

Sourceval declare_intopt_option_and_ref : (unit -> int option) opt_decl

Sourceval declare_nat_option_and_ref : (value:int -> unit -> int) opt_decl

Sourceval declare_bool_option_and_ref : (value:bool -> unit -> bool) opt_decl

Sourceval declare_string_option_and_ref : (value:string -> unit -> string) opt_decl

Sourceval declare_stringopt_option_and_ref : (unit -> string option) opt_decl

Source

val declare_interpreted_string_option_and_ref : 
  (value:'a -> (string -> 'a) -> ('a -> string) -> unit -> 'a) opt_decl

Special functions supposed to be used only in vernacentries.ml

Sourcemodule OptionMap : CSig.MapS with type key = option_name

Sourcetype 'a table_of_A = {

add : Environ.env -> 'a -> unit;
remove : Environ.env -> 'a -> unit;
mem : Environ.env -> 'a -> unit;
print : unit -> unit;

}

Sourceval get_string_table : option_name -> string table_of_A

Sourceval get_ref_table : option_name -> Libnames.qualid table_of_A

Source

val set_int_option_value_gen : 
  ?locality:option_locality ->
  option_name ->
  int option ->
  unit

The first argument is a locality flag.

Source

val set_bool_option_value_gen : 
  ?locality:option_locality ->
  option_name ->
  bool ->
  unit

Source

val set_string_option_value_gen : 
  ?locality:option_locality ->
  option_name ->
  string ->
  unit

Source

val set_string_option_append_value_gen : 
  ?locality:option_locality ->
  option_name ->
  string ->
  unit

Sourceval unset_option_value_gen : ?locality:option_locality -> option_name -> unit

Sourceval set_int_option_value : option_name -> int option -> unit

Sourceval set_bool_option_value : option_name -> bool -> unit

Sourceval set_string_option_value : option_name -> string -> unit

Sourceval print_option_value : option_name -> unit

Sourcetype option_value =

| BoolValue of bool
| IntValue of int option
| StringValue of string
| StringOptValue of string option

Sourcetype table_value =

| StringRefValue of string
| QualidRefValue of Libnames.qualid

Source

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.

Sourcetype option_state = {

opt_depr : bool;
opt_value : option_value;

}

Summary of an option status

Sourceval get_tables : unit -> option_state OptionMap.t

Sourceval print_tables : unit -> Pp.t

Sourcetype iter_table_aux = {

aux : 'a. 'a table_of_A -> Environ.env -> 'a -> unit;

}

Sourceval iter_table : iter_table_aux -> option_name -> table_value list -> unit

Sourceval error_undeclared_key : option_name -> 'a

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.library/Goptions/index.html

Module `Goptions`Source

Tables.

Options.

Special functions supposed to be used only in vernacentries.ml

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.library/Goptions/index.html

Module GoptionsSource

Tables.

Options.

Special functions supposed to be used only in vernacentries.ml

Module `Goptions`Source