Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et commandes vernaculaires (cf dev/changements.txt pour plus de précisions)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 22 insertions, 29 deletions

diff --git a/library/goptions.mli b/library/goptions.mli
index 8f810a266..d43a4283e 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -54,6 +54,7 @@
 
 (*i*)
 open Pp
+open Util
 open Names
 open Term
 open Nametab
@@ -68,26 +69,22 @@ type option_name =
 
 val error_undeclared_key : option_name -> 'a
 
-
 (*s Tables. *)
 
 (* The functor [MakeStringTable] declares a table containing objects
-   of type [string]; the function [check] is for testing if a given
-   object is allowed to be added to the table; 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 *)
+   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 :
   functor
     (A : sig
-       val check : string -> unit
        val key : option_name
        val title : string
-       val member_message : string -> bool -> string
+       val member_message : string -> bool -> std_ppcmds
        val synchronous : bool
      end) ->
 sig
@@ -95,29 +92,25 @@ sig
   val elements : unit -> string list
 end
 
-(* The functor [MakeIdentTable] declares a new table of [global_reference];
-   for generality, identifiers may be internally encode in other type
-   which is [A.t] through an encoding function [encode : global_reference ->
-   A.t] (typically, [A.t] is the persistent [global_reference] associated
-   to the currentdenotation of the [global_reference] and the encoding function
-   is the globalization function); the function [check] is for testing
-   if a given object is allowed to be added to the table; the function
+(* The functor [MakeRefTable] declares a new table of objects of type
+   [A.t] practically denoted by [qualid]; the encoding function
+   [encode : qualid -> 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.                                            *)
+   given object is in the table.  *)
 
-module MakeIdentTable :
+module MakeRefTable :
   functor
     (A : sig
            type t
-           val encode : global_reference -> t
-           val check : t -> unit
+           val encode : qualid located -> t
            val printer : t -> std_ppcmds
            val key : option_name
            val title : string
-           val member_message : global_reference -> bool -> string
+           val member_message : t -> bool -> std_ppcmds
            val synchronous : bool
          end) ->
     sig
@@ -145,7 +138,7 @@ type 'a option_sig = {
 
 type 'a write_function = 'a -> unit
 
-val declare_int_option   : int option_sig    -> int write_function
+val declare_int_option   : int option option_sig -> int option write_function
 val declare_bool_option  : bool option_sig   -> bool write_function
 val declare_string_option: string option_sig -> string write_function
 
@@ -159,14 +152,14 @@ val get_string_table :
       mem : string -> unit;
       print : unit >
 
-val get_ident_table :
+val get_ref_table :
   option_name ->
-    < add : global_reference -> unit;
-      remove : global_reference -> unit;
-      mem : global_reference -> unit;
+    < add : qualid located -> unit;
+      remove : qualid located -> unit;
+      mem : qualid located -> unit;
       print : unit >
 
-val set_int_option_value    : option_name -> int    -> unit
+val set_int_option_value    : option_name -> int option -> unit
 val set_bool_option_value   : option_name -> bool   -> unit
 val set_string_option_value : option_name -> string -> unit