1. matitaEngine splitted into disambiguation (now in grafite_parser) and

[helm.git] / helm / matita / matitaMisc.ml

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index 077809a17bc5eaac26d001878b116102f650e808..389ee2325683336d020ab506e88fea298e4861e5 100644 (file)
--- a/helm/matita/matitaMisc.ml
+++ b/helm/matita/matitaMisc.ml
@@ -24,27 +24,12 @@
  *)
 
 open Printf
-open MatitaTypes 
 
 (** Functions "imported" from Http_getter_misc *)
 
-let strip_trailing_slash = Http_getter_misc.strip_trailing_slash
 let normalize_dir = Http_getter_misc.normalize_dir
 let strip_suffix = Http_getter_misc.strip_suffix
 
-let baseuri_of_baseuri_decl st =
-  match st with
-  | GrafiteAst.Executable (_, GrafiteAst.Command (_, GrafiteAst.Set (_, "baseuri", buri))) ->
-      Some buri
-  | _ -> None
-
-let is_empty buri =
- List.for_all
-  (function
-      Http_getter_types.Ls_section _ -> true
-    | Http_getter_types.Ls_object _ -> false)
-  (Http_getter.ls (Http_getter_misc.strip_trailing_slash buri ^ "/"))
-
 let absolute_path file =
   if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file
   
@@ -163,42 +148,3 @@ let list_tl_at ?(equality=(==)) e l =
     | hd :: tl -> aux tl
   in
   aux l
-
-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 = 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 =
- if f = "coq.ma" then BuildTimeConf.coq_notation_script else
-  let baseuri = baseuri_of_file f in
-   LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri
-