From de26e97cf37cafd37b83377d2df062a6e82676e7 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Sun, 12 May 2013 15:33:40 +0000 Subject: Use the Hook module here and there. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16510 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/declare.ml | 26 ++++++++------------------ library/declare.mli | 9 +++------ library/declaremods.ml | 4 ---- library/declaremods.mli | 3 --- library/lib.ml | 11 ++++------- library/lib.mli | 4 ++-- library/library.ml | 7 +++---- library/library.mli | 2 +- 8 files changed, 21 insertions(+), 45 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index 4f88a6b0e..d664ebd0c 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -34,19 +34,12 @@ type internal_flag = (** XML output hooks *) -let xml_declare_variable = ref (fun (sp:object_name) -> ()) -let xml_declare_constant = ref (fun (sp:internal_flag * constant)-> ()) -let xml_declare_inductive = ref (fun (sp:internal_flag * object_name) -> ()) +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 () -let set_xml_declare_variable f = xml_declare_variable := if_xml f -let set_xml_declare_constant f = xml_declare_constant := if_xml f -let set_xml_declare_inductive f = xml_declare_inductive := if_xml f - -let cache_hook = ref ignore -let add_cache_hook f = cache_hook := f - (** Declaration of section variables and local definitions *) type section_variable_entry = @@ -94,7 +87,7 @@ let declare_variable id obj = declare_var_implicits id; Notation.declare_ref_arguments_scope (VarRef id); Heads.declare_head (EvalVarRef id); - !xml_declare_variable oname; + if_xml (Hook.get f_xml_declare_variable) oname; oname @@ -142,8 +135,7 @@ let cache_constant ((sp,kn), obj) = Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn)); add_section_constant kn' (Global.lookup_constant kn').const_hyps; Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps; - add_constant_kind (constant_of_kn kn) obj.cst_kind; - !cache_hook sp + add_constant_kind (constant_of_kn kn) obj.cst_kind let discharged_hyps kn sechyps = let (_,dir,_) = repr_kn kn in @@ -197,7 +189,7 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) = cst_locl = local; } in let kn = declare_constant_common id cst in - let () = !xml_declare_constant (internal, kn) in + let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in kn let declare_definition ?(internal=UserVerbose) @@ -260,9 +252,7 @@ let cache_inductive ((sp,kn),(dhyps,mie)) = assert (eq_mind kn' (mind_of_kn kn)); add_section_kn kn' (Global.lookup_mind kn').mind_hyps; Dischargedhypsmap.set_discharged_hyps sp dhyps; - List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names; - List.iter (fun (sp,_) -> !cache_hook sp) (inductive_names sp kn mie) - + List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names let discharge_inductive ((sp,kn),(dhyps,mie)) = let mind = Global.mind_of_delta_kn kn in @@ -306,7 +296,7 @@ let declare_mind isrecord mie = let mind = Global.mind_of_delta_kn kn in declare_mib_implicits mind; declare_inductive_argument_scopes mind mie; - !xml_declare_inductive (isrecord,oname); + if_xml (Hook.get f_xml_declare_inductive) (isrecord,oname); oname (* Declaration messages *) diff --git a/library/declare.mli b/library/declare.mli index a9cd8f720..ff4e20ad2 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -67,12 +67,9 @@ val declare_definition : val declare_mind : internal_flag -> mutual_inductive_entry -> object_name (** Hooks for XML output *) -val set_xml_declare_variable : (object_name -> unit) -> unit -val set_xml_declare_constant : (internal_flag * constant -> unit) -> unit -val set_xml_declare_inductive : (internal_flag * object_name -> unit) -> unit - -(** Hook for the cache function of constants and inductives *) -val add_cache_hook : (full_path -> unit) -> unit +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 *) diff --git a/library/declaremods.ml b/library/declaremods.ml index 894445de1..15a964792 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -600,11 +600,7 @@ let start_library dir = Lib.start_compilation dir mp; Lib.add_frozen_state () -let end_library_hook = ref ignore -let set_end_library_hook f = end_library_hook := f - let end_library dir = - !end_library_hook(); let prefix, lib_stack = Lib.end_compilation dir in let mp,cenv,ast = Global.export dir in let substitute, keep, _ = Lib.classify_segment lib_stack in diff --git a/library/declaremods.mli b/library/declaremods.mli index c5a43dfbf..06a4edd84 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -95,9 +95,6 @@ val end_library : library_name -> Safe_typing.compiled_library * library_objects * Safe_typing.native_library -(** set a function to be executed at end_library *) -val set_end_library_hook : (unit -> unit) -> unit - (** [really_import_module mp] opens the module [mp] (in a Caml sense). It modifies Nametab and performs the [open_object] function for every object of the module. Raises [Not_found] when [mp] is unknown. *) diff --git a/library/lib.ml b/library/lib.ml index 0ba9fd919..bf4c0a474 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -475,11 +475,8 @@ let is_in_section ref = (* Sections. *) (* XML output hooks *) -let xml_open_section = ref (fun id -> ()) -let xml_close_section = ref (fun id -> ()) - -let set_xml_open_section f = xml_open_section := f -let set_xml_close_section f = xml_close_section := f +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 @@ -493,7 +490,7 @@ 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 !xml_open_section id; + if !Flags.xml_export then Hook.get f_xml_open_section id; add_section () @@ -522,7 +519,7 @@ 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 !xml_close_section (basename (fst oname)); + 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 8ab98f775..c9b2047bc 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -178,8 +178,8 @@ val unfreeze : frozen -> unit val init : unit -> unit (** XML output hooks *) -val set_xml_open_section : (Names.Id.t -> unit) -> unit -val set_xml_close_section : (Names.Id.t -> unit) -> unit +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 * diff --git a/library/library.ml b/library/library.ml index 52d3a5d1d..472b1fb1d 100644 --- a/library/library.ml +++ b/library/library.ml @@ -498,8 +498,7 @@ let in_require : require_obj -> obj = (* Require libraries, import them if [export <> None], mark them for export if [export = Some true] *) -let xml_require = ref (fun d -> ()) -let set_xml_require f = xml_require := f +let (f_xml_require, xml_require) = Hook.make ~default:ignore () let require_library_from_dirpath modrefl export = let needed = List.fold_left rec_intern_library [] modrefl in @@ -514,7 +513,7 @@ let require_library_from_dirpath modrefl export = end else add_anonymous_leaf (in_require (needed,modrefl,export)); - if !Flags.xml_export then List.iter !xml_require modrefl; + if !Flags.xml_export then List.iter (Hook.get f_xml_require) modrefl; add_frozen_state () let require_library qidl export = @@ -531,7 +530,7 @@ let require_library_from_file idopt file export = end else add_anonymous_leaf (in_require (needed,[modref],export)); - if !Flags.xml_export then !xml_require modref; + 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 22b94e521..8ed3afd66 100644 --- a/library/library.mli +++ b/library/library.mli @@ -56,7 +56,7 @@ val library_full_filename : DirPath.t -> string val overwrite_library_filenames : string -> unit (** {6 Hook for the xml exportation of libraries } *) -val set_xml_require : (DirPath.t -> unit) -> unit +val xml_require : (DirPath.t -> unit) Hook.t (** {6 Locate a library in the load paths } *) exception LibUnmappedDir -- cgit v1.2.3