diff options
| author | filliatr | 2003-05-15 12:48:07 +0000 |
|---|---|---|
| committer | filliatr | 2003-05-15 12:48:07 +0000 |
| commit | 59dbc8ece1989efcf6e60278f8808d0dbce6bab0 (patch) | |
| tree | 7ad7249c627b11b746bb302739e67830c9897a92 | |
| parent | e3aef29b48e6f62abe8c5771320332004c132774 (diff) | |
table des modules charges (Library.compunit_cache) synchronizee (pour CoqIde notamment)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4025 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | ide/.cvsignore | 1 | ||||
| -rw-r--r-- | library/library.ml | 16 |
2 files changed, 11 insertions, 6 deletions
diff --git a/ide/.cvsignore b/ide/.cvsignore index 56eea49c95..47483fe10c 100644 --- a/ide/.cvsignore +++ b/ide/.cvsignore @@ -10,3 +10,4 @@ config_lexer.ml *.crashcoqide config_parser.mli config_parser.ml +utf8_convert.ml diff --git a/library/library.ml b/library/library.ml index 64e1272588..701fbcd971 100644 --- a/library/library.ml +++ b/library/library.ml @@ -142,23 +142,29 @@ let libraries_loaded_list = ref [] let libraries_imports_list = ref [] let libraries_exports_list = ref [] +(* cache for loaded libraries *) +let compunit_cache = ref CompilingLibraryMap.empty + let freeze () = !libraries_table, !libraries_loaded_list, !libraries_imports_list, - !libraries_exports_list + !libraries_exports_list, + !compunit_cache -let unfreeze (mt,mo,mi,me) = +let unfreeze (mt,mo,mi,me,cu) = libraries_table := mt; libraries_loaded_list := mo; libraries_imports_list := mi; - libraries_exports_list := me + libraries_exports_list := me; + compunit_cache := cu let init () = libraries_table := CompilingLibraryMap.empty; libraries_loaded_list := []; libraries_imports_list := []; - libraries_exports_list := [] + libraries_exports_list := []; + compunit_cache := CompilingLibraryMap.empty let _ = Summary.declare_summary "MODULES" @@ -258,8 +264,6 @@ let open_libraries export modl = (************************************************************************) (*s Loading from disk to cache (preparation phase) *) -let compunit_cache = ref CompilingLibraryMap.empty - let vo_magic_number = 0704 (* V7.4 *) let (raw_extern_library, raw_intern_library) = |