diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-12 22:12:02 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-08-01 18:42:44 +0200 |
commit | 2def58217686b5083da38778a5ebffb451b1d4d6 (patch) | |
tree | c0c2463a4620fe3c6bb2caf21a70f6861bbb4643 /library/lib.ml | |
parent | 65bd1deac80689d02be7ef580872974cc38bf93c (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.ml | 7 |
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; |