diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-12 08:11:14 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-12 08:11:14 +0000 |
| commit | 7a337e554e21f2943fa37f6ecee09e3b52be7772 (patch) | |
| tree | de5b003616122c688e1b42a89afd6b94a28fd1e9 /library | |
| parent | 91d8c7eda69c2e97d73dbc2922f3ba92b03a2b2f (diff) | |
Confusion sur commit précédent de library. La capture du Not_found
dans la recherche du nom long était bien utile (parce que la table des
filename n'est plus synchronisée et plus dans le initial.coq) mais
c'est ailleurs qu'on reposait à tort sur la bonne synchronisation de
la table des noms longs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11111 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
| -rw-r--r-- | library/library.ml | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/library/library.ml b/library/library.ml index da7c4ebb0..2f74fe92b 100644 --- a/library/library.ml +++ b/library/library.ml @@ -179,9 +179,6 @@ let _ = (* various requests to the tables *) -let exists_library dir = - LibraryMap.mem dir !libraries_table - let find_library dir = LibraryMap.find dir !libraries_table @@ -197,7 +194,8 @@ let register_library_filename dir f = LibraryFilenameMap.add dir f !libraries_filename_table let library_full_filename dir = - LibraryFilenameMap.find dir !libraries_filename_table + try LibraryFilenameMap.find dir !libraries_filename_table + with Not_found -> "<unavailable filename>" let library_is_loaded dir = try let _ = find_library dir in true @@ -345,9 +343,9 @@ let locate_absolute_library dir = (dir, file) with Not_found -> (* Last chance, removed from the file system but still in memory *) - try + if library_is_loaded dir then (dir, library_full_filename dir) - with Not_found -> + else raise LibNotFound let locate_qualified_library qid = @@ -365,7 +363,7 @@ let locate_qualified_library qid = let path, file = System.where_in_path loadpath name in let dir = extend_dirpath (find_logical_path path) base in (* Look if loaded *) - if exists_library dir then (LibLoaded, dir, library_full_filename dir) + if library_is_loaded dir then (LibLoaded, dir, library_full_filename dir) (* Otherwise, look for it in the file system *) else (LibInPath, dir, file) with Not_found -> raise LibNotFound @@ -460,7 +458,7 @@ let rec_intern_by_filename_only id f = (* Only the base name is expected to match *) check_library_short_name f m.library_name id; (* We check no other file containing same library is loaded *) - if exists_library m.library_name then + if library_is_loaded m.library_name then begin Flags.if_verbose warning ((string_of_dirpath m.library_name)^" is already loaded from file "^ |