X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitacleanLib.ml;h=82fac08af78a1a7516719a9ab78733be4e1e8e5d;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=e8a1fd29a301bf1141f4ae2739929664aa2f9426;hpb=595d77eece3202a799e786ac5996b6b1e25fac6e;p=helm.git

diff --git a/helm/matita/matitacleanLib.ml b/helm/matita/matitacleanLib.ml
index e8a1fd29a..82fac08af 100644
--- a/helm/matita/matitacleanLib.ml
+++ b/helm/matita/matitacleanLib.ml
@@ -227,3 +227,41 @@ let clean_baseuris ?(verbose=true) buris =
       MetadataTypes.count_tbl()]
    end
 
+let baseuri_of_file file = 
+  let uri = ref None in
+  let ic = open_in file in
+  let istream = Ulexing.from_utf8_channel ic in
+  (try
+    while true do
+      try 
+        let stm = GrafiteParser.parse_statement istream in
+        match MatitaMisc.baseuri_of_baseuri_decl stm with
+        | Some buri -> 
+            let u = MatitaMisc.strip_trailing_slash buri in
+            if String.length u < 5 || String.sub u 0 5 <> "cic:/" then
+              MatitaLog.error (file ^ " sets an incorrect baseuri: " ^ buri);
+            (try 
+              ignore(Http_getter.resolve u)
+            with
+            | Http_getter_types.Unresolvable_URI _ -> 
+                MatitaLog.error (file ^ " sets an unresolvable baseuri: "^buri)
+            | Http_getter_types.Key_not_found _ -> ());
+            uri := Some u;
+            raise End_of_file
+        | None -> ()
+      with
+        CicNotationParser.Parse_error _ as exn ->
+          prerr_endline ("Unable to parse: " ^ file);
+          prerr_endline (MatitaExcPp.to_string exn);
+          ()
+    done
+  with End_of_file -> close_in ic);
+  match !uri with
+  | Some uri -> uri
+  | None -> failwith ("No baseuri defined in " ^ file)
+
+let obj_file_of_script f =
+ if f = "coq.ma" then BuildTimeConf.coq_notation_script else
+  let baseuri = baseuri_of_file f in
+   MatitaMisc.obj_file_of_baseuri baseuri
+