Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.

1 files changed, 3 insertions, 0 deletions

diff --git a/library/library.ml b/library/library.ml
index 024ac9e6fa..365d119ddf 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -555,6 +555,8 @@ let in_require : require_obj -> obj =
 (* Require libraries, import them if [export <> None], mark them for export
    if [export = Some true] *)
 
+let (f_xml_require, xml_require) = Hook.make ~default:ignore ()
+
 let require_library_from_dirpath modrefl export =
   let needed, contents = List.fold_left rec_intern_library ([], DPMap.empty) modrefl in
   let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in
@@ -568,6 +570,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 (Hook.get f_xml_require) modrefl;
   add_frozen_state ()
 
 (* the function called by Vernacentries.vernac_import *)