Bug fixed: heuristic to detect real URIs used to raise an exception.

[helm.git] / matita / components / grafite_parser / dependenciesParser.ml

diff --git a/matita/components/grafite_parser/dependenciesParser.ml b/matita/components/grafite_parser/dependenciesParser.ml
index 53fb7ab6d63b8cdf5f845f9fe7c68d0d0e72532c..57370660a7f8449e5e170fb24d6ffeb5e2b0a0b2 100644 (file)
--- a/matita/components/grafite_parser/dependenciesParser.ml
+++ b/matita/components/grafite_parser/dependenciesParser.ml
@@ -30,12 +30,12 @@ exception UnableToInclude of string
   (* statements meaningful for matitadep *)
 type dependency =
   | IncludeDep of string
-  | UriDep of UriManager.uri
+  | UriDep of NUri.uri
   | InlineDep of string
 
 let pp_dependency = function
   | IncludeDep str -> "include \"" ^ str ^ "\""
-  | UriDep uri -> "uri \"" ^ UriManager.string_of_uri uri ^ "\""
+  | UriDep uri -> "uri \"" ^ NUri.string_of_uri uri ^ "\""
   | InlineDep str -> "inline \"" ^ str ^ "\"" 
 
 let parse_dependencies lexbuf = 
@@ -49,11 +49,12 @@ let parse_dependencies lexbuf =
       | [< '("QSTRING", s) >] ->
           (* because of alias id qstring = qstring :-( *)
           (try
-            true, (UriDep (UriManager.uri_of_string s) :: acc)
-           with
-            UriManager.IllFormedUri _ -> true, acc)
+            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 (UriManager.uri_of_string u) :: acc)
+          true, (UriDep (NUri.uri_of_string u) :: acc)
       | [< '("IDENT", "include"); '("QSTRING", fname) >] ->
           true, (IncludeDep fname :: acc)
       | [< '("IDENT", "include"); '("IDENT", "source"); '("QSTRING", fname) >] ->