Removing dead code relative to the XML plugin.

6 files changed, 0 insertions, 33 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 94239d0bf..8ec52d16a 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -32,14 +32,6 @@ type internal_flag =
   | KernelSilent  (* kernel action, no message is displayed *)
   | UserVerbose   (* user action, a message is displayed *)
 
-(** XML output hooks *)
-
-let (f_xml_declare_variable, xml_declare_variable) = Hook.make ~default:ignore ()
-let (f_xml_declare_constant, xml_declare_constant) = Hook.make ~default:ignore ()
-let (f_xml_declare_inductive, xml_declare_inductive) = Hook.make ~default:ignore ()
-
-let if_xml f x = if !Flags.xml_export then f x else ()
-
 (** Declaration of section variables and local definitions *)
 
 type section_variable_entry =
@@ -91,7 +83,6 @@ let declare_variable id obj =
   declare_var_implicits id;
   Notation.declare_ref_arguments_scope (VarRef id);
   Heads.declare_head (EvalVarRef id);
-  if_xml (Hook.get f_xml_declare_variable) oname;
   oname
 
 
@@ -291,7 +282,6 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) =
     cst_locl = local;
   } in
   let kn = declare_constant_common id cst in
-  let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in
   kn
 
 let declare_definition ?(internal=UserVerbose) 
@@ -412,7 +402,6 @@ let declare_mind isrecord mie =
   declare_projections mind;
   declare_mib_implicits mind;
   declare_inductive_argument_scopes mind mie;
-  if_xml (Hook.get f_xml_declare_inductive) (isrecord,oname);
   oname
 
 (* Declaration messages *)
diff --git a/library/declare.mli b/library/declare.mli
index a9fd8956e..bda90229e 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -70,11 +70,6 @@ val set_declare_scheme :
    the whole block (boolean must be true iff it is a record) *)
 val declare_mind : internal_flag -> mutual_inductive_entry -> object_name
 
-(** Hooks for XML output *)
-val xml_declare_variable : (object_name -> unit) Hook.t
-val xml_declare_constant : (internal_flag * constant -> unit) Hook.t
-val xml_declare_inductive : (internal_flag * object_name -> unit) Hook.t
-
 (** Declaration messages *)
 
 val definition_message : Id.t -> unit
diff --git a/library/lib.ml b/library/lib.ml
index f33f244b8..d85d38368 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -475,10 +475,6 @@ let full_section_segment_of_constant con =
 (*************)
 (* 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) = !path_prefix in
   let dir = add_dirpath_suffix olddir id in
@@ -490,7 +486,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);
   path_prefix := prefix;
-  if !Flags.xml_export then Hook.get f_xml_open_section id;
   add_section ()
 
 
@@ -519,7 +514,6 @@ let close_section () =
   let full_olddir = fst !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 b5a32f762..8e4ea4c21 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -156,10 +156,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 = Names.Id.t * Decl_kinds.binding_kind *
     Term.constr option * Term.types
diff --git a/library/library.ml b/library/library.ml
index 9552a6ca9..7bff05cda 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -600,8 +600,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 require_library_from_dirpath modrefl export =
   let needed, contents = List.fold_left rec_intern_library ([], DPMap.empty) modrefl in
   let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in
@@ -615,7 +613,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;
   add_frozen_state ()
 
 let require_library qidl export =
@@ -632,7 +629,6 @@ let require_library_from_file idopt file export =
   end
   else
     add_anonymous_leaf (in_require (needed,[modref],export));
-  if !Flags.xml_export then Hook.get f_xml_require modref;
   add_frozen_state ()
 
 (* the function called by Vernacentries.vernac_import *)
diff --git a/library/library.mli b/library/library.mli
index 0f6f510d8..5154c25e4 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -66,9 +66,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