diff options
| -rw-r--r-- | library/lib.ml | 15 | ||||
| -rw-r--r-- | library/summary.mli | 1 | ||||
| -rw-r--r-- | toplevel/stm.ml | 7 |
3 files changed, 17 insertions, 6 deletions
diff --git a/library/lib.ml b/library/lib.ml index 6bbf8ef47..eef8171cc 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -516,10 +516,19 @@ let freeze ~marshallable = match marshallable with | `Shallow -> (* TASSI: we should do something more sensible here *) - let _, initial_prefix = - CList.split_when (function _, CompilingLibrary _ -> true | _ -> false) + let lib_stk = + CList.map_filter (function + | _, Leaf _ -> None + | n, (CompilingLibrary _ as x) -> Some (n,x) + | n, OpenedModule (it,e,op,_) -> + Some(n,OpenedModule(it,e,op,Summary.empty_frozen)) + | n, ClosedModule _ -> Some (n,ClosedModule []) + | n, OpenedSection (op, _) -> + Some(n,OpenedSection(op,Summary.empty_frozen)) + | n, ClosedSection _ -> Some (n,ClosedSection []) + | _, FrozenState _ -> None) !lib_stk in - !comp_name, initial_prefix + !comp_name, lib_stk | _ -> !comp_name, !lib_stk diff --git a/library/summary.mli b/library/summary.mli index f6a9c6951..1ce09e12c 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -57,6 +57,7 @@ val nop : unit -> unit type frozen +val empty_frozen : frozen val freeze_summaries : marshallable:marshallable -> frozen val unfreeze_summaries : frozen -> unit val init_summaries : unit -> unit diff --git a/toplevel/stm.ml b/toplevel/stm.ml index c0ad01758..790a65107 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -1277,9 +1277,10 @@ let known_state ?(redefine_qed=false) ~cache id = | `MaybeASync (start, nodes, ids) -> (fun () -> prerr_endline ("MaybeAsynchronous " ^ Stateid.to_string id); reach ~cache:`Shallow start; - (* no sections and no modules *) - if List.is_empty (Environ.named_context (Global.env ())) && - Safe_typing.is_curmod_library (Global.safe_env ()) then + (* no sections *) + if List.is_empty (Environ.named_context (Global.env ())) + (* && Safe_typing.is_curmod_library (Global.safe_env ()) *) + then fst (aux (`ASync (start, None, nodes,ids))) () else fst (aux (`Sync `Unknown)) () |