]> matita.cs.unibo.it Git - helm.git/commitdiff
Bug fixed: heuristic to detect real URIs used to raise an exception.
authorAndrea Asperti <andrea.asperti@unibo.it>
Wed, 27 Oct 2010 09:55:21 +0000 (09:55 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Wed, 27 Oct 2010 09:55:21 +0000 (09:55 +0000)
matita/components/grafite_parser/dependenciesParser.ml

index 6b0142bf12233a544c2dd2f34b3b18c3b064d366..57370660a7f8449e5e170fb24d6ffeb5e2b0a0b2 100644 (file)
@@ -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) >] ->