[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.

6 files changed, 1 insertions, 43 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index e7aa5bd0d..6d9295bde 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -557,17 +557,6 @@ let openmodtype_info =
   Summary.ref ([] : module_type_body list) ~name:"MODTYPE-INFO"
 
 
-(** XML output hooks *)
-
-let (f_xml_declare_module, xml_declare_module) = Hook.make ~default:ignore ()
-let (f_xml_start_module, xml_start_module) = Hook.make ~default:ignore ()
-let (f_xml_end_module, xml_end_module) = Hook.make ~default:ignore ()
-let (f_xml_declare_module_type, xml_declare_module_type) = Hook.make ~default:ignore ()
-let (f_xml_start_module_type, xml_start_module_type) = Hook.make ~default:ignore ()
-let (f_xml_end_module_type, xml_end_module_type) = Hook.make ~default:ignore ()
-
-let if_xml f x = if !Flags.xml_export then f x else ()
-
 (** {6 Modules : start, end, declare} *)
 
 module RawModOps = struct
@@ -589,7 +578,6 @@ let start_module interp_modast export id args res fs =
   openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps };
   let prefix = Lib.start_module export id mp fs in
   Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix);
-  if_xml (Hook.get f_xml_start_module) mp;
   mp
 
 let end_module () =
@@ -628,7 +616,6 @@ let end_module () =
   assert (eq_full_path (fst newoname) (fst oldoname));
   assert (ModPath.equal (mp_of_kn (snd newoname)) mp);
 
-  if_xml (Hook.get f_xml_end_module) mp;
   mp
 
 let declare_module interp_modast id args res mexpr_o fs =
@@ -682,7 +669,6 @@ let declare_module interp_modast id args res mexpr_o fs =
 
   let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in
   ignore (Lib.add_leaf id (in_module sobjs));
-  if_xml (Hook.get f_xml_declare_module) mp;
   mp
 
 end
@@ -699,7 +685,6 @@ let start_modtype interp_modast id args mtys fs =
   openmodtype_info := sub_mty_l;
   let prefix = Lib.start_modtype id mp fs in
   Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix);
-  if_xml (Hook.get f_xml_start_module_type) mp;
   mp
 
 let end_modtype () =
@@ -716,7 +701,6 @@ let end_modtype () =
   assert (eq_full_path (fst oname) (fst oldoname));
   assert (ModPath.equal (mp_of_kn (snd oname)) mp);
 
-  if_xml (Hook.get f_xml_end_module_type) mp;
   mp
 
 let declare_modtype interp_modast id args mtys (mty,ann) fs =
@@ -750,7 +734,6 @@ let declare_modtype interp_modast id args mtys (mty,ann) fs =
   check_subtypes_mt mp sub_mty_l;
 
   ignore (Lib.add_leaf id (in_modtype sobjs));
-  if_xml (Hook.get f_xml_declare_module_type) mp;
   mp
 
 end
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 005594b8d..9d750b616 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -63,14 +63,6 @@ val start_modtype :
 
 val end_modtype : unit -> module_path
 
-(** Hooks for XML output *)
-val xml_declare_module : (module_path -> unit) Hook.t
-val xml_start_module : (module_path -> unit) Hook.t
-val xml_end_module : (module_path -> unit) Hook.t
-val xml_declare_module_type : (module_path -> unit) Hook.t
-val xml_start_module_type : (module_path -> unit) Hook.t
-val xml_end_module_type : (module_path -> unit) Hook.t
-
 (** {6 Libraries i.e. modules on disk } *)
 
 type library_name = DirPath.t
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;
diff --git a/library/lib.mli b/library/lib.mli
index f1c9bfca2..3dcec1d53 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -150,10 +150,6 @@ val unfreeze : frozen -> unit
 
 val init : unit -> unit
 
-(** XML output hooks *)
-val xml_open_section : (Names.Id.t -> unit) Hook.t
-val xml_close_section : (Names.Id.t -> unit) Hook.t
-
 (** {6 Section management for discharge } *)
 type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
 type variable_context = variable_info list 
@@ -165,7 +161,7 @@ val named_of_variable_context : variable_context -> Context.Named.t
 val section_segment_of_constant : Names.constant -> abstr_info
 val section_segment_of_mutual_inductive: Names.mutual_inductive -> abstr_info
 val variable_section_segment_of_reference : Globnames.global_reference -> variable_context
-                                                                                                     
+
 val section_instance : Globnames.global_reference -> Univ.universe_instance * Names.Id.t array
 val is_in_section : Globnames.global_reference -> bool
 
diff --git a/library/library.ml b/library/library.ml
index 20ecc2c22..28afa054e 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -551,8 +551,6 @@ 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 warn_require_in_module =
   CWarnings.create ~name:"require-in-module" ~category:"deprecated"
                    (fun () -> strbrk "Require inside a module is" ++
@@ -574,7 +572,6 @@ 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;
   ()
 
 (* the function called by Vernacentries.vernac_import *)
diff --git a/library/library.mli b/library/library.mli
index 604167804..6c624ce52 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -67,9 +67,6 @@ val library_full_filename : DirPath.t -> string
   (** - Overwrite the filename of all libraries (used when restoring a state) *)
 val overwrite_library_filenames : string -> unit
 
-(** {6 Hook for the xml exportation of libraries } *)
-val xml_require : (DirPath.t -> unit) Hook.t
-
 (** {6 Locate a library in the load paths } *)
 exception LibUnmappedDir
 exception LibNotFound