aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/lib.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-06-12 22:12:02 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-08-01 18:42:44 +0200
commit2def58217686b5083da38778a5ebffb451b1d4d6 (patch)
treec0c2463a4620fe3c6bb2caf21a70f6861bbb4643 /library/lib.ml
parent65bd1deac80689d02be7ef580872974cc38bf93c (diff)
[flags] Remove XML output flag.
This is a second try at removing the hooks for the legacy xml export system which can't currently be tested. It is also not included in the API, so it should either be included in it or this PR be applied.
Diffstat (limited to 'library/lib.ml')
-rw-r--r--library/lib.ml7
1 files changed, 0 insertions, 7 deletions
diff --git a/library/lib.ml b/library/lib.ml
index a24d20c68..c6a0253b3 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -512,11 +512,6 @@ let is_in_section ref =
(*************)
(* Sections. *)
-
-(* XML output hooks *)
-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) = !lib_state.path_prefix in
let dir = add_dirpath_suffix olddir id in
@@ -528,7 +523,6 @@ 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);
lib_state := { !lib_state with path_prefix = prefix };
- if !Flags.xml_export then Hook.get f_xml_open_section id;
add_section ()
@@ -556,7 +550,6 @@ let close_section () =
let full_olddir = fst !lib_state.path_prefix in
pop_path_prefix ();
add_entry oname (ClosedSection (List.rev (mark::secdecls)));
- 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;