]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/grafite2/grafiteMisc.ml
1. Several files in grafite that should be in grafite_parser moved there.
[helm.git] / helm / ocaml / grafite2 / grafiteMisc.ml
index 8739b7a070fb4c70c2a0b997432684c04197fe6f..227cd382b955cf1a349739ddc8b7d01b1727fcd5 100644 (file)
@@ -29,51 +29,3 @@ let is_empty buri =
       Http_getter_types.Ls_section _ -> true
     | Http_getter_types.Ls_object _ -> false)
   (Http_getter.ls (Http_getter_misc.strip_trailing_slash buri ^ "/"))
-
-let baseuri_of_baseuri_decl st =
-  match st with
-  | GrafiteAst.Executable (_, GrafiteAst.Command (_, GrafiteAst.Set (_, "baseuri", buri))) ->
-      Some buri
-  | _ -> None
-
-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 baseuri_of_baseuri_decl stm with
-        | Some buri -> 
-            let u = Http_getter_misc.strip_trailing_slash buri in
-            if String.length u < 5 || String.sub u 0 5 <> "cic:/" then
-              HLog.error (file ^ " sets an incorrect baseuri: " ^ buri);
-            (try 
-              ignore(Http_getter.resolve u)
-            with
-            | Http_getter_types.Unresolvable_URI _ -> 
-                HLog.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 err ->
-          HLog.error ("Unable to parse: " ^ file);
-          HLog.error ("Parse error: " ^ err);
-          ()
-    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 ~basedir f =
-  let baseuri = baseuri_of_file f in
-   LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri
-
-let metadata_file_of_script ~basedir f =
-  let baseuri = baseuri_of_file f in
-   LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri
-