From 51d38d0892eae4a253356e52614da6dee6513e9e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 8 Sep 2014 19:38:27 +0200 Subject: Removing dead code relative to the XML plugin. --- library/declare.ml | 11 ----------- library/declare.mli | 5 ----- library/lib.ml | 6 ------ library/lib.mli | 4 ---- library/library.ml | 4 ---- library/library.mli | 3 --- 6 files changed, 33 deletions(-) (limited to 'library') 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 -- cgit v1.2.3