From b108ab28153129d6578d7d9c2ffdf19e6779d86f Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 27 Oct 2010 09:55:21 +0000 Subject: [PATCH] Bug fixed: heuristic to detect real URIs used to raise an exception. --- matita/components/grafite_parser/dependenciesParser.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/matita/components/grafite_parser/dependenciesParser.ml b/matita/components/grafite_parser/dependenciesParser.ml index 6b0142bf1..57370660a 100644 --- a/matita/components/grafite_parser/dependenciesParser.ml +++ b/matita/components/grafite_parser/dependenciesParser.ml @@ -48,9 +48,11 @@ let parse_dependencies lexbuf = (parser | [< '("QSTRING", s) >] -> (* because of alias id qstring = qstring :-( *) - if String.sub s 0 5 <> "cic:/" then true,acc - else - true, (UriDep (NUri.uri_of_string s) :: acc) + (try + if String.sub s 0 5 <> "cic:/" then true,acc + else + true, (UriDep (NUri.uri_of_string s) :: acc) + with Invalid_argument _ -> true,acc) | [< '("URI", u) >] -> true, (UriDep (NUri.uri_of_string u) :: acc) | [< '("IDENT", "include"); '("QSTRING", fname) >] -> -- 2.39.2