From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 library/goptions.mli | 45 ++++++++++++++++++++-------------------------
 1 file changed, 20 insertions(+), 25 deletions(-)

(limited to 'library/goptions.mli')

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
-- 
cgit v1.2.3