Crochets pour exported les sections en xml

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

2 files changed, 14 insertions, 0 deletions

diff --git a/library/lib.ml b/library/lib.ml
index ea22acca5..c5bc798d9 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -378,6 +378,13 @@ let is_module () =
 (* Returns the most recent OpenedThing node *)
 let what_is_opened () = find_entry_p is_something_opened
 
+(* 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
+
 (* Sections. *)
 
 let open_section id =
@@ -392,6 +399,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 !Options.xml_export then !xml_open_section id;
   prefix
 
 
@@ -417,6 +425,7 @@ let close_section ~export id =
   in
   let name = make_path id, make_kn id in
   add_entry name closed_sec;
+  if !Options.xml_export then !xml_close_section id;
   (prefix, after, fs)
 
 (* Backtracking. *)
diff --git a/library/lib.mli b/library/lib.mli
index d9448f310..6ff3e4601 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -149,3 +149,8 @@ val init : unit -> unit
 
 val declare_initial_state : unit -> unit
 val reset_initial : unit -> unit
+
+
+(* XML output hooks *)
+val set_xml_open_section : (identifier -> unit) -> unit
+val set_xml_close_section : (identifier -> unit) -> unit