aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-06-12 12:37:55 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-06-12 12:40:10 +0200
commit63896b2443e71e47c016fc9d0709cc22cf24f288 (patch)
tree4f618edca12168797703fe0d6c2d88cbd1b6d541 /library
parent79c42e22dd5106dcb85229ceec75331029ab5486 (diff)
[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.
Diffstat (limited to 'library')
-rw-r--r--library/declaremods.ml7
-rw-r--r--library/lib.ml13
-rw-r--r--library/lib.mli5
-rw-r--r--library/library.ml2
4 files changed, 4 insertions, 23 deletions
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 *)