Use the Hook module here and there.

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

8 files changed, 21 insertions, 45 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 4f88a6b0e..d664ebd0c 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -34,19 +34,12 @@ type internal_flag =
 
 (** XML output hooks *)
 
-let xml_declare_variable = ref (fun (sp:object_name) -> ())
-let xml_declare_constant = ref (fun (sp:internal_flag * constant)-> ())
-let xml_declare_inductive = ref (fun (sp:internal_flag * object_name) -> ())
+let (f_xml_declare_variable, xml_declare_variable) = Hook.make ~default:ignore ()
+let (f_xml_declare_constant, xml_declare_constant) = Hook.make ~default:ignore ()
+let (f_xml_declare_inductive, xml_declare_inductive) = Hook.make ~default:ignore ()
 
 let if_xml f x = if !Flags.xml_export then f x else ()
 
-let set_xml_declare_variable f = xml_declare_variable := if_xml f
-let set_xml_declare_constant f = xml_declare_constant := if_xml f
-let set_xml_declare_inductive f = xml_declare_inductive := if_xml f
-
-let cache_hook = ref ignore
-let add_cache_hook f = cache_hook := f
-
 (** Declaration of section variables and local definitions *)
 
 type section_variable_entry =
@@ -94,7 +87,7 @@ let declare_variable id obj =
   declare_var_implicits id;
   Notation.declare_ref_arguments_scope (VarRef id);
   Heads.declare_head (EvalVarRef id);
-  !xml_declare_variable oname;
+  if_xml (Hook.get f_xml_declare_variable) oname;
   oname
 
 
@@ -142,8 +135,7 @@ let cache_constant ((sp,kn), obj) =
   Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
   add_section_constant kn' (Global.lookup_constant kn').const_hyps;
   Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps;
-  add_constant_kind (constant_of_kn kn) obj.cst_kind;
-  !cache_hook sp
+  add_constant_kind (constant_of_kn kn) obj.cst_kind
 
 let discharged_hyps kn sechyps =
   let (_,dir,_) = repr_kn kn in
@@ -197,7 +189,7 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) =
     cst_locl = local;
   } in
   let kn = declare_constant_common id cst in
-  let () = !xml_declare_constant (internal, kn) in
+  let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in
   kn
 
 let declare_definition ?(internal=UserVerbose)
@@ -260,9 +252,7 @@ let cache_inductive ((sp,kn),(dhyps,mie)) =
   assert (eq_mind kn' (mind_of_kn kn));
   add_section_kn kn' (Global.lookup_mind kn').mind_hyps;
   Dischargedhypsmap.set_discharged_hyps sp dhyps;
-  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names;
-  List.iter (fun (sp,_) -> !cache_hook sp) (inductive_names sp kn mie)
-
+  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
 
 let discharge_inductive ((sp,kn),(dhyps,mie)) =
   let mind = Global.mind_of_delta_kn kn in
@@ -306,7 +296,7 @@ let declare_mind isrecord mie =
   let mind = Global.mind_of_delta_kn kn in
   declare_mib_implicits mind;
   declare_inductive_argument_scopes mind mie;
-  !xml_declare_inductive (isrecord,oname);
+  if_xml (Hook.get f_xml_declare_inductive) (isrecord,oname);
   oname
 
 (* Declaration messages *)
diff --git a/library/declare.mli b/library/declare.mli
index a9cd8f720..ff4e20ad2 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -67,12 +67,9 @@ val declare_definition :
 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 : (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
+val xml_declare_variable : (object_name -> unit) Hook.t
+val xml_declare_constant : (internal_flag * constant -> unit) Hook.t
+val xml_declare_inductive : (internal_flag * object_name -> unit) Hook.t
 
 (** Declaration messages *)
 
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 894445de1..15a964792 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -600,11 +600,7 @@ let start_library dir =
   Lib.start_compilation dir mp;
   Lib.add_frozen_state ()
 
-let end_library_hook = ref ignore
-let set_end_library_hook f = end_library_hook := f
-
 let end_library dir =
-  !end_library_hook();
   let prefix, lib_stack = Lib.end_compilation dir in
   let mp,cenv,ast = Global.export dir in
   let substitute, keep, _ = Lib.classify_segment lib_stack in
diff --git a/library/declaremods.mli b/library/declaremods.mli
index c5a43dfbf..06a4edd84 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -95,9 +95,6 @@ val end_library :
   library_name ->
     Safe_typing.compiled_library * library_objects * Safe_typing.native_library
 
-(** set a function to be executed at end_library *)
-val set_end_library_hook : (unit -> unit) -> unit
-
 (** [really_import_module mp] opens the module [mp] (in a Caml sense).
    It modifies Nametab and performs the [open_object] function for
    every object of the module. Raises [Not_found] when [mp] is unknown. *)
diff --git a/library/lib.ml b/library/lib.ml
index 0ba9fd919..bf4c0a474 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -475,11 +475,8 @@ let is_in_section ref =
 (* Sections. *)
 
 (* XML output hooks *)
-let xml_open_section = ref (fun id -> ())
-let xml_close_section = ref (fun id -> ())
-
-let set_xml_open_section f = xml_open_section := f
-let set_xml_close_section f = xml_close_section := f
+let (f_xml_open_section, xml_open_section) = Hook.make ~default:ignore ()
+let (f_xml_close_section, xml_close_section) = Hook.make ~default:ignore ()
 
 let open_section id =
   let olddir,(mp,oldsec) = !path_prefix in
@@ -493,7 +490,7 @@ let open_section id =
   (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
   Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
   path_prefix := prefix;
-  if !Flags.xml_export then !xml_open_section id;
+  if !Flags.xml_export then Hook.get f_xml_open_section id;
   add_section ()
 
 
@@ -522,7 +519,7 @@ let close_section () =
   let full_olddir = fst !path_prefix in
   pop_path_prefix ();
   add_entry oname (ClosedSection (List.rev (mark::secdecls)));
-  if !Flags.xml_export then !xml_close_section (basename (fst oname));
+  if !Flags.xml_export then Hook.get f_xml_close_section (basename (fst oname));
   let newdecls = List.map discharge_item secdecls in
   Summary.unfreeze_summaries fs;
   List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls;
diff --git a/library/lib.mli b/library/lib.mli
index 8ab98f775..c9b2047bc 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -178,8 +178,8 @@ val unfreeze : frozen -> unit
 val init : unit -> unit
 
 (** XML output hooks *)
-val set_xml_open_section : (Names.Id.t -> unit) -> unit
-val set_xml_close_section : (Names.Id.t -> unit) -> unit
+val xml_open_section : (Names.Id.t -> unit) Hook.t
+val xml_close_section : (Names.Id.t -> unit) Hook.t
 
 (** {6 Section management for discharge } *)
 type variable_info = Names.Id.t * Decl_kinds.binding_kind *
diff --git a/library/library.ml b/library/library.ml
index 52d3a5d1d..472b1fb1d 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -498,8 +498,7 @@ let in_require : require_obj -> obj =
 (* Require libraries, import them if [export <> None], mark them for export
    if [export = Some true] *)
 
-let xml_require = ref (fun d -> ())
-let set_xml_require f = xml_require := f
+let (f_xml_require, xml_require) = Hook.make ~default:ignore ()
 
 let require_library_from_dirpath modrefl export =
   let needed = List.fold_left rec_intern_library [] modrefl in
@@ -514,7 +513,7 @@ let require_library_from_dirpath modrefl export =
       end
     else
       add_anonymous_leaf (in_require (needed,modrefl,export));
-    if !Flags.xml_export then List.iter !xml_require modrefl;
+    if !Flags.xml_export then List.iter (Hook.get f_xml_require) modrefl;
   add_frozen_state ()
 
 let require_library qidl export =
@@ -531,7 +530,7 @@ let require_library_from_file idopt file export =
   end
   else
     add_anonymous_leaf (in_require (needed,[modref],export));
-  if !Flags.xml_export then !xml_require modref;
+  if !Flags.xml_export then Hook.get f_xml_require modref;
   add_frozen_state ()
 
 (* the function called by Vernacentries.vernac_import *)
diff --git a/library/library.mli b/library/library.mli
index 22b94e521..8ed3afd66 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -56,7 +56,7 @@ val library_full_filename : DirPath.t -> string
 val overwrite_library_filenames : string -> unit
 
 (** {6 Hook for the xml exportation of libraries } *)
-val set_xml_require : (DirPath.t -> unit) -> unit
+val xml_require : (DirPath.t -> unit) Hook.t
 
 (** {6 Locate a library in the load paths } *)
 exception LibUnmappedDir