diff options
Diffstat (limited to 'library/goptions.mli')
| -rw-r--r-- | library/goptions.mli | 45 |
1 files changed, 20 insertions, 25 deletions
diff --git a/library/goptions.mli b/library/goptions.mli index 3b3651f3..6c14d19e 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This module manages customization parameters at the vernacular level *) @@ -40,15 +42,16 @@ Unset Tata Tutu Titi. Print Table Tata Tutu Titi. (** synonym: Test Table Tata Tutu Titi. *) - The created table/option may be declared synchronous or not - (synchronous = consistent with the resetting commands) *) + All options are synchronized with the document. +*) -open Pp open Libnames open Mod_subst type option_name = string list +type option_locality = OptDefault | OptLocal | OptExport | OptGlobal + (** {6 Tables. } *) (** The functor [MakeStringTable] declares a table containing objects @@ -64,8 +67,7 @@ module MakeStringTable : (A : sig val key : option_name val title : string - val member_message : string -> bool -> std_ppcmds - val synchronous : bool + val member_message : string -> bool -> Pp.t end) -> sig val active : string -> bool @@ -89,11 +91,10 @@ module MakeRefTable : val compare : t -> t -> int val encode : reference -> t val subst : substitution -> t -> t - val printer : t -> std_ppcmds + val printer : t -> Pp.t val key : option_name val title : string - val member_message : t -> bool -> std_ppcmds - val synchronous : bool + val member_message : t -> bool -> Pp.t end) -> sig val active : A.t -> bool @@ -108,8 +109,6 @@ module MakeRefTable : used when printing the option value (command "Print Toto Titi." *) type 'a option_sig = { - optsync : bool; - (** whether the option is synchronous w.r.t to the section/module system. *) optdepr : bool; (** whether the option is DEPRECATED *) optname : string; @@ -120,8 +119,6 @@ type 'a option_sig = { optwrite : 'a -> unit } -(** When an option is declared synchronous ([optsync] is [true]), the output is - a synchronous write function. Otherwise it is [optwrite] *) (** 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. *) @@ -155,13 +152,12 @@ val get_ref_table : mem : reference -> unit; print : unit > -(** The first argument is a locality flag. - [Some true] = "Local", [Some false]="Global". *) -val set_int_option_value_gen : bool option -> option_name -> int option -> unit -val set_bool_option_value_gen : bool option -> option_name -> bool -> unit -val set_string_option_value_gen : bool option -> option_name -> string -> unit -val set_string_option_append_value_gen : bool option -> option_name -> string -> unit -val unset_option_value_gen : bool option -> option_name -> unit +(** The first argument is a locality flag. *) +val set_int_option_value_gen : ?locality:option_locality -> option_name -> int option -> unit +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 @@ -177,13 +173,12 @@ type option_value = (** Summary of an option status *) type option_state = { - opt_sync : bool; opt_depr : bool; opt_name : string; opt_value : option_value; } val get_tables : unit -> option_state OptionMap.t -val print_tables : unit -> std_ppcmds +val print_tables : unit -> Pp.t val error_undeclared_key : option_name -> 'a |