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

10 files changed, 85 insertions, 45 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
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 1cf74025ab..a64ae57f56 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -906,7 +906,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
   let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in
   let mie,impls = Command.interp_mutual_inductive indl [] true (* means: not coinductive *) in
   (* Declare the mutual inductive block with its associated schemes *)
-  ignore (Command.declare_mutual_inductive_with_eliminations false mie impls)
+  ignore (Command.declare_mutual_inductive_with_eliminations Declare.UserVerbose mie impls)
 
 
 (* Find infos on identifier id. *)
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 676863b782..336ae2ccde 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -408,7 +408,11 @@ let kind_of_global_goal = function
 let kind_of_inductive isrecord kn =
  "DEFINITION",
  if (fst (Global.lookup_inductive (kn,0))).Declarations.mind_finite
- then if isrecord then "Record" else "Inductive"
+ then begin 
+   match isrecord with 
+   | Declare.KernelSilent -> "Record"
+   | _ -> "Inductive"
+ end
  else "CoInductive"
 ;;
 
@@ -478,8 +482,8 @@ let kind_of_global r =
   match r with
   | Ln.IndRef kn | Ln.ConstructRef (kn,_) ->
       let isrecord =
-	try let _ = Recordops.lookup_projections kn in true
-        with Not_found -> false in
+	try let _ = Recordops.lookup_projections kn in Declare.KernelSilent
+        with Not_found -> Declare.KernelVerbose in
       kind_of_inductive isrecord (fst kn)
   | Ln.VarRef id -> kind_of_variable id
   | Ln.ConstRef kn -> kind_of_constant kn
@@ -539,13 +543,15 @@ let print internal glob_ref kind xml_library_root =
   in
   let fn = filename_of_path xml_library_root tag in
   let uri = Cic2acic.uri_of_kernel_name tag in
-   if not internal then print_object_kind uri kind;
+  (match internal with
+    | Declare.KernelSilent -> ()
+    | _ -> print_object_kind uri kind);
    print_object uri obj Evd.empty None fn
 ;;
 
 let print_ref qid fn =
   let ref = Nametab.global qid in
-  print false ref (kind_of_global ref) fn
+  print Declare.UserVerbose ref (kind_of_global ref) fn
 
 (* show dest                                                  *)
 (*  where dest is either None (for stdout) or (Some filename) *)
@@ -580,7 +586,7 @@ let _ =
   Declare.set_xml_declare_variable
    (function (sp,kn) ->
      let id = Libnames.basename sp in
-     print false (Libnames.VarRef id) (kind_of_variable id) xml_library_root ;
+     print Declare.UserVerbose (Libnames.VarRef id) (kind_of_variable id) xml_library_root ;
      proof_to_export := None)
 ;;
 
@@ -603,7 +609,8 @@ let _ =
 let _ =
   Declare.set_xml_declare_inductive
    (function (isrecord,(sp,kn)) ->
-      print false (Libnames.IndRef (Names.mind_of_kn kn,0)) (kind_of_inductive isrecord (Names.mind_of_kn kn))
+      print Declare.UserVerbose (Libnames.IndRef (Names.mind_of_kn kn,0))
+        (kind_of_inductive isrecord (Names.mind_of_kn kn))
         xml_library_root)
 ;;
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 4259ccb81c..21fb277e2b 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -363,7 +363,7 @@ let do_mutual_inductive indl finite =
   (* Interpret the types *)
   let mie,impls = interp_mutual_inductive indl ntns finite in
   (* Declare the mutual inductive block with its associated schemes *)
-  ignore (declare_mutual_inductive_with_eliminations false mie impls);
+  ignore (declare_mutual_inductive_with_eliminations UserVerbose mie impls);
   (* Declare the possible notations of inductive types *)
   List.iter Metasyntax.add_notation_interpretation ntns;
   (* Declare the coercions *)
diff --git a/toplevel/command.mli b/toplevel/command.mli
index b056afa58d..779e77f313 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -82,7 +82,7 @@ val interp_mutual_inductive :
    associated schemes *)
 
 val declare_mutual_inductive_with_eliminations :
-  bool -> mutual_inductive_entry -> one_inductive_impls list ->
+  Declare.internal_flag -> mutual_inductive_entry -> one_inductive_impls list ->
   mutual_inductive
 
 (** Entry points for the vernacular commands Inductive and CoInductive *)
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 8e3d9437f8..4e8d861000 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -110,7 +110,11 @@ let declare_scheme kind indcl =
   Lib.add_anonymous_leaf (inScheme (kind,indcl))
 
 let define internal id c =
-  let fd = if internal then declare_internal_constant else declare_constant in
+  (* TODO: specify even more by distinguish between KernelVerbose and
+   * UserVerbose *)
+  let fd = match internal with 
+    | KernelSilent -> declare_internal_constant
+    | _ -> declare_constant in
   let kn = fd id
     (DefinitionEntry
       { const_entry_body = c;
@@ -118,7 +122,9 @@ let define internal id c =
         const_entry_opaque = false;
 	const_entry_boxed = Flags.boxed_definitions() },
       Decl_kinds.IsDefinition Scheme) in
-  if not internal then definition_message id;
+  (match internal with
+  | KernelSilent -> ()
+  | _-> definition_message id);
   kn
 
 let define_individual_scheme_base kind suff f internal idopt (mind,i as ind) =
@@ -153,14 +159,15 @@ let define_mutual_scheme kind internal names mind =
   | s,MutualSchemeFunction f ->
       define_mutual_scheme_base kind s f internal names mind
 
+(* TODO: change KernelSilent here to the right behaviour *)
 let find_scheme kind (mind,i as ind) =
   try Stringmap.find kind (Indmap.find ind !scheme_map)
   with Not_found ->
   match Hashtbl.find scheme_object_table kind with
   | s,IndividualSchemeFunction f ->
-      define_individual_scheme_base kind s f true None ind
+      define_individual_scheme_base kind s f KernelSilent None ind
   | s,MutualSchemeFunction f ->
-      (define_mutual_scheme_base kind s f true [] mind).(i)
+      (define_mutual_scheme_base kind s f KernelSilent [] mind).(i)
 
 let check_scheme kind ind =
   try let _ = Stringmap.find kind (Indmap.find ind !scheme_map) in true
diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli
index 0d3a250c95..babc2d9209 100644
--- a/toplevel/ind_tables.mli
+++ b/toplevel/ind_tables.mli
@@ -39,10 +39,11 @@ val declare_scheme : 'a scheme_kind -> (inductive * constant) array -> unit
 
 (** Force generation of a (mutually) scheme with possibly user-level names *)
 
-val define_individual_scheme : individual scheme_kind -> bool (** internal *) ->
+val define_individual_scheme : individual scheme_kind -> 
+  Declare.internal_flag (** internal *) ->
   identifier option -> inductive -> constant
 
-val define_mutual_scheme : mutual scheme_kind -> bool (** internal *) ->
+val define_mutual_scheme : mutual scheme_kind -> Declare.internal_flag (** internal *) ->
   (int * identifier) list -> mutual_inductive -> constant array
 
 (** Main function to retrieve a scheme in the cache or to generate it *)
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index a02b01351f..03813c9d48 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -100,7 +100,10 @@ let _ =
 (* Util *)
 
 let define id internal c t =
-  let f = if internal then declare_internal_constant else declare_constant in
+  (* TODO: specify even more by distinguish KernelVerbose and UserVerbose *)
+  let f = match internal with
+   | KernelSilent -> declare_internal_constant
+   | _ -> declare_constant in
   let kn = f id
     (DefinitionEntry
       { const_entry_body = c;
@@ -118,12 +121,13 @@ let declare_beq_scheme_gen internal names kn =
 
 let alarm what internal msg =
   let debug = false in
-  if internal then
+  (* TODO: specify even more by distinguish KernelVerbose and UserVerbose *)
+  match internal with
+  | KernelSilent ->
     (if debug then
       Flags.if_verbose Pp.msg_warning
 	(hov 0 msg ++ fnl () ++ what ++ str " not defined."))
-  else
-    errorlabstrm "" msg
+  | _ -> errorlabstrm "" msg
 
 let try_declare_scheme what f internal names kn =
   try f internal names kn
@@ -164,18 +168,19 @@ let beq_scheme_msg mind =
     (list_tabulate (fun i -> (mind,i)) (Array.length mib.mind_packets))
 
 let declare_beq_scheme_with l kn =
-  try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen false l kn
+  try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen UserVerbose l kn
 
+(* TODO : maybe switch to KernelVerbose to have the right behaviour *)
 let try_declare_beq_scheme kn =
   (* TODO: handle Fix, see e.g. TheoryList.In_spec, eventually handle
       proof-irrelevance; improve decidability by depending on decidability
       for the parameters rather than on the bl and lb properties *)
-  try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen true [] kn
+  try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen KernelSilent [] kn
 
 let declare_beq_scheme = declare_beq_scheme_with []
 
 (* Case analysis schemes *)
-
+(* TODO: maybe switch to KernelVerbose *)
 let declare_one_case_analysis_scheme ind =
   let (mib,mip) = Global.lookup_inductive ind in
   let kind = inductive_sort_family mip in
@@ -185,7 +190,7 @@ let declare_one_case_analysis_scheme ind =
        induction scheme, the other ones share the same code with the
        apropriate type *)
   if List.mem InType kelim then
-    ignore (define_individual_scheme dep true None ind)
+    ignore (define_individual_scheme dep KernelSilent None ind)
 
 (* Induction/recursion schemes *)
 
@@ -199,6 +204,7 @@ let kinds_from_type =
    InProp,ind_dep_scheme_kind_from_type;
    InSet,rec_dep_scheme_kind_from_type]
 
+(* TODO: maybe switch to kernel verbose *)
 let declare_one_induction_scheme ind =
   let (mib,mip) = Global.lookup_inductive ind in
   let kind = inductive_sort_family mip in
@@ -208,7 +214,7 @@ let declare_one_induction_scheme ind =
     list_map_filter (fun (sort,kind) ->
       if List.mem sort kelim then Some kind else None)
       (if from_prop then kinds_from_prop else kinds_from_type) in
-  List.iter (fun kind -> ignore (define_individual_scheme kind true None ind))
+  List.iter (fun kind -> ignore (define_individual_scheme kind KernelSilent None ind))
     elims
 
 let declare_induction_schemes kn =
@@ -231,45 +237,50 @@ let eq_dec_scheme_msg ind = (* TODO: mutual inductive case *)
 
 let declare_eq_decidability_scheme_with l kn =
   try_declare_scheme (eq_dec_scheme_msg (kn,0))
-    declare_eq_decidability_gen false l kn
+    declare_eq_decidability_gen UserVerbose l kn
 
+(* TODO:  maybe switch to kernel verbose *)
 let try_declare_eq_decidability kn =
   try_declare_scheme (eq_dec_scheme_msg (kn,0))
-    declare_eq_decidability_gen true [] kn
+    declare_eq_decidability_gen KernelSilent [] kn
 
 let declare_eq_decidability = declare_eq_decidability_scheme_with []
 
 let ignore_error f x = try ignore (f x) with _ -> ()
 
+(* TODO: maybe switch to kernel verbose *)
 let declare_rewriting_schemes ind =
   if Hipattern.is_inductive_equality ind then begin
-    ignore (define_individual_scheme rew_r2l_scheme_kind true None ind);
-    ignore (define_individual_scheme rew_r2l_dep_scheme_kind true None ind);
-    ignore (define_individual_scheme rew_r2l_forward_dep_scheme_kind true None ind);
+    ignore (define_individual_scheme rew_r2l_scheme_kind KernelSilent None ind);
+    ignore (define_individual_scheme rew_r2l_dep_scheme_kind KernelSilent None ind);
+    ignore (define_individual_scheme rew_r2l_forward_dep_scheme_kind
+      KernelSilent None ind);
     (* These ones expect the equality to be symmetric; the first one also *)
     (* needs eq *)
-    ignore_error (define_individual_scheme rew_l2r_scheme_kind true None) ind;
+    ignore_error (define_individual_scheme rew_l2r_scheme_kind KernelSilent None) ind;
     ignore_error
-      (define_individual_scheme rew_l2r_dep_scheme_kind true None) ind;
+      (define_individual_scheme rew_l2r_dep_scheme_kind KernelSilent None) ind;
     ignore_error
-      (define_individual_scheme rew_l2r_forward_dep_scheme_kind true None) ind
+      (define_individual_scheme rew_l2r_forward_dep_scheme_kind KernelSilent None) ind
   end
 
+(* TODO: maybe switch to kernel verbose *)
 let declare_congr_scheme ind =
   if Hipattern.is_equality_type (mkInd ind) then begin
     if
       try Coqlib.check_required_library Coqlib.logic_module_name; true
       with _ -> false
     then
-      ignore (define_individual_scheme congr_scheme_kind true None ind)
+      ignore (define_individual_scheme congr_scheme_kind KernelSilent None ind)
     else
       warning "Cannot build congruence scheme because eq is not found"
   end
 
+(* TODO: maybe switch to kernel verbose *)
 let declare_sym_scheme ind =
   if Hipattern.is_inductive_equality ind then
     (* Expect the equality to be symmetric *)
-    ignore_error (define_individual_scheme sym_scheme_kind true None) ind
+    ignore_error (define_individual_scheme sym_scheme_kind KernelSilent None) ind
 
 (* Scheme command *)
 
@@ -337,7 +348,7 @@ let do_mutual_induction_scheme lnamedepindsort =
   let rec declare decl fi lrecref =
     let decltype = Retyping.get_type_of env0 Evd.empty decl in
     let decltype = refresh_universes decltype in
-    let cst = define fi false decl (Some decltype) in
+    let cst = define fi UserVerbose decl (Some decltype) in
     ConstRef cst :: lrecref
   in
   let _ = List.fold_right2 declare listdecl lrecnames [] in
@@ -432,7 +443,7 @@ let do_combined_scheme name schemes =
       schemes
   in
   let body,typ = build_combined_scheme (Global.env ()) csts in
-  ignore (define (snd name) false body (Some typ));
+  ignore (define (snd name) UserVerbose body (Some typ));
   fixpoint_message None [snd name]
 
 (**********************************************************************)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index e4177b0fc1..89bf769114 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -259,7 +259,8 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls
       mind_entry_record = true;
       mind_entry_finite = recursivity_flag_of_kind finite;
       mind_entry_inds = [mie_ind] } in
-  let kn = Command.declare_mutual_inductive_with_eliminations true mie [(paramimpls,[])] in
+(* TODO : maybe switch to KernelVerbose *)
+  let kn = Command.declare_mutual_inductive_with_eliminations KernelSilent mie [(paramimpls,[])] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
   let cstr = (rsp,1) in
   let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in