From 63896b2443e71e47c016fc9d0709cc22cf24f288 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 12 Jun 2017 12:37:55 +0200 Subject: [lib] Remove obsolete state-management function add_frozen_state AFAICS this function predates modern state-handling; nowadays summaries are stored by the STM and nobody were using this information. --- library/declaremods.ml | 7 +------ library/lib.ml | 13 ++----------- library/lib.mli | 5 ----- library/library.ml | 2 +- 4 files changed, 4 insertions(+), 23 deletions(-) (limited to 'library') diff --git a/library/declaremods.ml b/library/declaremods.ml index c98d4a7f3..187b749b8 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -589,7 +589,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); - Lib.add_frozen_state (); if_xml (Hook.get f_xml_start_module) mp; mp @@ -629,7 +628,6 @@ let end_module () = assert (eq_full_path (fst newoname) (fst oldoname)); assert (ModPath.equal (mp_of_kn (snd newoname)) mp); - Lib.add_frozen_state () (* to prevent recaching *); if_xml (Hook.get f_xml_end_module) mp; mp @@ -701,7 +699,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); - Lib.add_frozen_state (); if_xml (Hook.get f_xml_start_module_type) mp; mp @@ -719,7 +716,6 @@ let end_modtype () = assert (eq_full_path (fst oname) (fst oldoname)); assert (ModPath.equal (mp_of_kn (snd oname)) mp); - Lib.add_frozen_state ()(* to prevent recaching *); if_xml (Hook.get f_xml_end_module_type) mp; mp @@ -894,8 +890,7 @@ let get_library_native_symbols dir = let start_library dir = let mp = Global.start_library dir in openmod_info := default_module_info; - Lib.start_compilation dir mp; - Lib.add_frozen_state () + Lib.start_compilation dir mp let end_library_hook = ref ignore let append_end_library_hook f = diff --git a/library/lib.ml b/library/lib.ml index 9d71a854f..f22f53ead 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -27,7 +27,6 @@ type node = | ClosedModule of library_segment | OpenedSection of object_prefix * Summary.frozen | ClosedSection of library_segment - | FrozenState of Summary.frozen and library_entry = object_name * node @@ -80,7 +79,6 @@ let classify_segment seg = | (_,OpenedModule (ty,_,_,_)) :: _ -> user_err ~hdr:"Lib.classify_segment" (str "there are still opened " ++ str (module_kind ty) ++ str "s") - | (_,FrozenState _) :: stk -> clean acc stk in clean ([],[],[]) (List.rev seg) @@ -254,10 +252,6 @@ let add_anonymous_leaf ?(cache_first = true) obj = cache_object (oname,obj) end -let add_frozen_state () = - add_anonymous_entry - (FrozenState (Summary.freeze_summaries ~marshallable:`No)) - (* Modules. *) let is_opening_node = function @@ -544,7 +538,6 @@ let discharge_item ((sp,_ as oname),e) = match e with | Leaf lobj -> Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj)) - | FrozenState _ -> None | ClosedSection _ | ClosedModule _ -> None | OpenedSection _ | OpenedModule _ | CompilingLibrary _ -> anomaly (Pp.str "discharge_item.") @@ -585,8 +578,7 @@ let freeze ~marshallable = | n, ClosedModule _ -> Some (n,ClosedModule []) | n, OpenedSection (op, _) -> Some(n,OpenedSection(op,Summary.empty_frozen)) - | n, ClosedSection _ -> Some (n,ClosedSection []) - | _, FrozenState _ -> None) + | n, ClosedSection _ -> Some (n,ClosedSection [])) !lib_state.lib_stk in { !lib_state with lib_stk } | _ -> @@ -596,8 +588,7 @@ let unfreeze st = lib_state := st let init () = unfreeze initial_lib_state; - Summary.init_summaries (); - add_frozen_state () (* Stores e.g. the keywords declared in g_*.ml4 *) + Summary.init_summaries () (* Misc *) diff --git a/library/lib.mli b/library/lib.mli index 9f9d8c7e5..f47d6e1a5 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -23,7 +23,6 @@ type node = | ClosedModule of library_segment | OpenedSection of Libnames.object_prefix * Summary.frozen | ClosedSection of library_segment - | FrozenState of Summary.frozen and library_segment = (Libnames.object_name * node) list @@ -61,8 +60,6 @@ val pull_to_head : Libnames.object_name -> unit for each of them *) val add_leaves : Names.Id.t -> Libobject.obj list -> Libnames.object_name -val add_frozen_state : unit -> unit - (** {6 ... } *) (** The function [contents] gives access to the current entire segment *) @@ -123,8 +120,6 @@ val end_modtype : Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment -(** [Lib.add_frozen_state] must be called after each of the above functions *) - (** {6 Compilation units } *) val start_compilation : Names.DirPath.t -> Names.module_path -> unit diff --git a/library/library.ml b/library/library.ml index 5a5f99cc5..db05ad2b7 100644 --- a/library/library.ml +++ b/library/library.ml @@ -575,7 +575,7 @@ let require_library_from_dirpath modrefl export = 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 () + () (* the function called by Vernacentries.vernac_import *) -- cgit v1.2.3