X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FdependenciesParser.ml;h=74cf0aa774333592b5ed396aab97581a38cd678b;hb=14d7eabdb425c4dbcda5de18fac0735fde5d176b;hp=dee9511182333c36d1ff7412f3c6498103e1b475;hpb=b95be966e385957a25f26a41f45e0116955264ae;p=helm.git diff --git a/helm/software/components/grafite_parser/dependenciesParser.ml b/helm/software/components/grafite_parser/dependenciesParser.ml index dee951118..74cf0aa77 100644 --- a/helm/software/components/grafite_parser/dependenciesParser.ml +++ b/helm/software/components/grafite_parser/dependenciesParser.ml @@ -43,6 +43,7 @@ let parse_dependencies lexbuf = CicNotationLexer.level2_ast_lexer.Token.tok_func (Obj.magic lexbuf) in let rec parse acc = + try (parser | [< '("URI", u) >] -> parse (UriDep (UriManager.uri_of_string u) :: acc) @@ -53,6 +54,8 @@ let parse_dependencies lexbuf = | [< '("EOI", _) >] -> acc | [< 'tok >] -> parse acc | [< >] -> acc) tok_stream + with + Stream.Error _ -> parse acc in List.rev (parse []) @@ -83,10 +86,4 @@ let baseuri_of_script ~include_paths file = let uri = Http_getter_misc.strip_trailing_slash buri in if String.length uri < 5 || String.sub uri 0 5 <> "cic:/" then HLog.error (file ^ " sets an incorrect baseuri: " ^ buri); - (try - ignore(Http_getter.resolve ~writable:false uri) - with - | Http_getter_types.Unresolvable_URI _ -> - HLog.error (file ^ " sets an unresolvable baseuri: " ^ buri) - | Http_getter_types.Key_not_found _ -> ()); - uri + uri,file