X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatitadep.ml;h=5b22cb70b9cbe9abce580c4d254a0344b009a3d4;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=3eb83af00964690ebf276127c9fa44f3e1a412c3;hpb=afe21e48aefe81db3ca150fac9a5bbfbc893fa59;p=helm.git diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml index 3eb83af00..5b22cb70b 100644 --- a/helm/matita/matitadep.ml +++ b/helm/matita/matitadep.ml @@ -26,36 +26,32 @@ module GA = GrafiteAst module U = UriManager -(* all are maps from "file" to "something" *) -let include_deps = Hashtbl.create (Array.length Sys.argv) -let baseuri_of = Hashtbl.create (Array.length Sys.argv) -let uri_deps = Hashtbl.create (Array.length Sys.argv) - -let buri alias = - U.buri_of_uri (U.uri_of_string alias) - -let resolve alias current_buri= - let buri = buri alias in - if buri <> current_buri then Some buri else None - -let find path = - let rec aux = function - | [] -> close_in (open_in path); path - | p :: tl -> - try - close_in (open_in (p ^ "/" ^ path)); p ^ "/" ^ path - with Sys_error _ -> aux tl - in - let paths = Helm_registry.get_list Helm_registry.string "matita.includes" in - try - aux paths - with Sys_error _ as exc -> - MatitaLog.error ("Unable to read " ^ path); - MatitaLog.error ("opts.include_paths was " ^ String.concat ":" paths); - raise exc -;; - let main () = + (* all are maps from "file" to "something" *) + let include_deps = Hashtbl.create (Array.length Sys.argv) in + let baseuri_of = Hashtbl.create (Array.length Sys.argv) in + let uri_deps = Hashtbl.create (Array.length Sys.argv) in + let buri alias = U.buri_of_uri (U.uri_of_string alias) in + let resolve alias current_buri = + let buri = buri alias in + if buri <> current_buri then Some buri else None + in + let find path = + let rec aux = function + | [] -> close_in (open_in path); path + | p :: tl -> + try + close_in (open_in (p ^ "/" ^ path)); p ^ "/" ^ path + with Sys_error _ -> aux tl + in + let paths = Helm_registry.get_list Helm_registry.string "matita.includes" in + try + aux paths + with Sys_error _ as exc -> + MatitaLog.error ("Unable to read " ^ path); + MatitaLog.error ("opts.include_paths was " ^ String.concat ":" paths); + raise exc + in MatitaInit.load_configuration_file (); MatitaInit.parse_cmdline (); List.iter @@ -75,7 +71,7 @@ let main () = | GrafiteAst.IncludeDep path -> try let ma_file = if path <> "coq.ma" then find path else path in - let moo_file = MatitaMisc.obj_file_of_script ma_file in + let moo_file = MatitacleanLib.obj_file_of_script ma_file in Hashtbl.add include_deps file moo_file with Sys_error _ -> MatitaLog.warn @@ -96,11 +92,8 @@ let main () = let deps = List.fast_sort Pervasives.compare deps in let deps = HExtlib.list_uniq deps in let deps = file :: deps in - let moo = MatitaMisc.obj_file_of_script file in + let moo = MatitacleanLib.obj_file_of_script file in Printf.printf "%s: %s\n" moo (String.concat " " deps); Printf.printf "%s: %s\n" (Pcre.replace ~pat:"ma$" ~templ:"mo" file) moo) (Helm_registry.get_list Helm_registry.string "matita.args") -;; - -let _ = - main () +