+ (* 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 ();