X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatitadep.ml;h=48011c0b5300cde4643667d7be8bca91e9352b5b;hb=6355ac16ff3996e16d9d9cfb08e4184bc7962f8b;hp=e93dbad61ad379b4b1e671c36cd9f6cd092807af;hpb=41be5e85a1103a5b14495bb487995a6a88e79c48;p=helm.git diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml index e93dbad61..48011c0b5 100644 --- a/helm/matita/matitadep.ml +++ b/helm/matita/matitadep.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + module GA = GrafiteAst module U = UriManager @@ -44,22 +46,25 @@ let main () = (fun ma_file -> let ic = open_in ma_file in let istream = Ulexing.from_utf8_channel ic in - let dependencies = GrafiteParser.parse_dependencies istream in + let dependencies = DependenciesParser.parse_dependencies istream in close_in ic; List.iter (function - | GrafiteAst.UriDep uri -> + | DependenciesParser.UriDep uri -> let uri = UriManager.string_of_uri uri in - Hashtbl.add uri_deps ma_file uri - | GrafiteAst.BaseuriDep uri -> + if not (Http_getter_storage.is_legacy uri) then + Hashtbl.add uri_deps ma_file uri + | DependenciesParser.BaseuriDep uri -> let uri = Http_getter_misc.strip_trailing_slash uri in Hashtbl.add baseuri_of ma_file uri - | GrafiteAst.IncludeDep path -> + | DependenciesParser.IncludeDep path -> try let baseuri = - GrafiteParserMisc.baseuri_of_script ~include_paths path in - let moo_file = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in - Hashtbl.add include_deps ma_file moo_file + DependenciesParser.baseuri_of_script ~include_paths path in + if not (Http_getter_storage.is_legacy baseuri) then + let moo_file = + LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in + Hashtbl.add include_deps ma_file moo_file with Sys_error _ -> HLog.warn ("Unable to find " ^ path ^ " that is included in " ^ ma_file)