change the flag "internal" in declare/ind_tables from bool to

a 3 state type to allow:
 * KernelVerbose / KernelSilent : handle the display of messages launch by Coq
 * UserVerbose : handle the display of messages launch by user actions

Coq will still behaves the same way (TODOs in the code mark the places
where we can now change the behaviour). I'll remove them in a few days
when we'll have agreed on the correct behaviour.



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

2 files changed, 20 insertions, 7 deletions

diff --git a/library/declare.ml b/library/declare.ml
index b571ecf3a4..2886c63d85 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -25,11 +25,17 @@ open Cooking
 open Decls
 open Decl_kinds
 
+(** flag for internal message display *)
+type internal_flag = 
+  | KernelVerbose (* kernel action, a message is displayed *)
+  | KernelSilent  (* kernel action, no message is displayed *)
+  | UserVerbose   (* user action, a message is displayed *)
+
 (** XML output hooks *)
 
 let xml_declare_variable = ref (fun (sp:object_name) -> ())
-let xml_declare_constant = ref (fun (sp:bool * constant)-> ())
-let xml_declare_inductive = ref (fun (sp:bool * object_name) -> ())
+let xml_declare_constant = ref (fun (sp:internal_flag * constant)-> ())
+let xml_declare_inductive = ref (fun (sp:internal_flag * object_name) -> ())
 
 let if_xml f x = if !Flags.xml_export then f x else ()
 
@@ -172,8 +178,10 @@ let declare_constant_gen internal id (cd,kind) =
   !xml_declare_constant (internal,kn);
   kn
 
-let declare_internal_constant = declare_constant_gen true
-let declare_constant = declare_constant_gen false
+(* TODO: add a third function to distinguish between KernelVerbose
+ * and user Verbose *)
+let declare_internal_constant = declare_constant_gen KernelSilent
+let declare_constant = declare_constant_gen UserVerbose
 
 (** Declaration of inductive blocks *)
 
diff --git a/library/declare.mli b/library/declare.mli
index 3ff91cc5e7..3847a4ab94 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -44,6 +44,11 @@ type constant_declaration = constant_entry * logical_kind
 (** [declare_constant id cd] declares a global declaration
    (constant/parameter) with name [id] in the current section; it returns
    the full path of the declaration *)
+type internal_flag =
+  | KernelVerbose
+  | KernelSilent
+  | UserVerbose
+
 val declare_constant :
  identifier -> constant_declaration -> constant
 
@@ -53,12 +58,12 @@ val declare_internal_constant :
 (** [declare_mind me] declares a block of inductive types with
    their constructors in the current section; it returns the path of
    the whole block (boolean must be true iff it is a record) *)
-val declare_mind : bool -> mutual_inductive_entry -> object_name
+val declare_mind : internal_flag -> mutual_inductive_entry -> object_name
 
 (** Hooks for XML output *)
 val set_xml_declare_variable : (object_name -> unit) -> unit
-val set_xml_declare_constant : (bool * constant -> unit) -> unit
-val set_xml_declare_inductive : (bool * object_name -> unit) -> unit
+val set_xml_declare_constant : (internal_flag * constant -> unit) -> unit
+val set_xml_declare_inductive : (internal_flag * object_name -> unit) -> unit
 
 (** Hook for the cache function of constants and inductives *)
 val add_cache_hook : (full_path -> unit) -> unit