diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-08 18:52:47 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-08 18:52:47 +0000 |
| commit | 80aba8d52c650ef8e4ada694c20bf12c15849694 (patch) | |
| tree | 74a6bba0cf4661a2b1319c7b94e6a4f165becadc /library/library.ml | |
| parent | b9d45d500d6cb12494bd6cb41bbe29a9bbb9ffd3 (diff) | |
enhance marshallable option for freeze (minor TODO in safe_typing)
It can be:
`Yes Full data, in a state that can be marshalled
`No Full data, good for Undo only
`Shallow Partial data, marshallable, good for slave processes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16682 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/library.ml')
| -rw-r--r-- | library/library.ml | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/library/library.ml b/library/library.ml index 0766a62d7..472b1fb1d 100644 --- a/library/library.ml +++ b/library/library.ml @@ -44,20 +44,17 @@ module LibraryOrdered = DirPath module LibraryMap = Map.Make(LibraryOrdered) module LibraryFilenameMap = Map.Make(LibraryOrdered) -let join x = Safe_typing.join_compiled_library x.library_compiled (* This is a map from names to loaded libraries *) -let freeze b l = if b then (LibraryMap.iter (fun _ x -> join x) l; l) else l -let libraries_table = Summary.ref LibraryMap.empty ~name:"LIBRARY" ~freeze +let libraries_table = Summary.ref LibraryMap.empty ~name:"LIBRARY" (* This is the map of loaded libraries filename *) (* (not synchronized so as not to be caught in the states on disk) *) let libraries_filename_table = ref LibraryFilenameMap.empty (* These are the _ordered_ sets of loaded, imported and exported libraries *) -let freeze b l = if b then (List.iter join l; l) else l -let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD" ~freeze -let libraries_imports_list = Summary.ref [] ~name:"LIBRARY-IMPORT" ~freeze -let libraries_exports_list = Summary.ref [] ~name:"LIBRARY-EXPORT" ~freeze +let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD" +let libraries_imports_list = Summary.ref [] ~name:"LIBRARY-IMPORT" +let libraries_exports_list = Summary.ref [] ~name:"LIBRARY-EXPORT" (* various requests to the tables *) |