Merge PR #773: [flags] Remove XML output flag.

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 dc903df09..5418003eb 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -521,11 +521,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
@@ -537,7 +532,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 ()
 
 
@@ -565,7 +559,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