diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/lib.ml | 9 | ||||
| -rw-r--r-- | library/lib.mli | 5 |
2 files changed, 14 insertions, 0 deletions
diff --git a/library/lib.ml b/library/lib.ml index ea22acca5f..c5bc798d9b 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 d9448f3102..6ff3e46010 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 |