X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatitadep.ml;h=e355ab59c9efeaff8ca90a642114104e0e25d64d;hb=cec61c8b027b15b98d308cee8900d9cf35a02d28;hp=56c60aff8cc40f7885f28c07e9c11c9e3649d702;hpb=6b5e1d495c61f459738187e8d71efadb162abdbe;p=helm.git diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml index 56c60aff8..e355ab59c 100644 --- a/helm/matita/matitadep.ml +++ b/helm/matita/matitadep.ml @@ -39,7 +39,7 @@ module TA = GrafiteAst module U = UriManager let deps = Hashtbl.create (Array.length Sys.argv) -let baseuri = ref [] +let baseuris = ref [] let aliases = Hashtbl.create (Array.length Sys.argv) (* @@ -53,10 +53,8 @@ let buri alias = U.buri_of_uri (U.uri_of_string alias) let resolve alias = - try - Some (snd(List.find (fun (u, f) -> u = (buri alias)) !baseuri)) - with - | Not_found -> None + let buri = buri alias in + if List.exists (fun u -> u = buri) !baseuris then Some buri else None (*** TODO MANCANO LE URI VERBATIM DENTRO GLI AST DEI TERMINI ****) @@ -82,49 +80,56 @@ let main () = CicNotation.load_notation BuildTimeConf.core_notation_script; let files = ref [] in Arg.parse arg_spec (add_l files) usage; - List.iter (fun file -> + List.iter + (fun file -> let ic = open_in file in let istream = Stream.of_channel ic in (try while true do - match GrafiteParser.parse_statement istream with - | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", uri))) -> - let uri = MatitaMisc.strip_trailing_slash uri in - baseuri := (uri, file) :: !baseuri - | TA.Executable (_, TA.Command - (_, TA.Alias (_, TA.Ident_alias(_, uri)))) -> - Hashtbl.add aliases file uri - | TA.Executable (_, TA.Command (_, TA.Include (_, path))) -> - Hashtbl.add deps file (find path) - | _ -> () + try + match GrafiteParser.parse_statement istream with + | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", uri))) -> + let uri = MatitaMisc.strip_trailing_slash uri in + baseuris := uri :: !baseuris + | TA.Executable (_, TA.Command + (_, TA.Alias (_, TA.Ident_alias(_, uri)))) -> + Hashtbl.add aliases file uri + | TA.Executable (_, TA.Command (_, TA.Include (_, path))) -> + (try + Hashtbl.add deps file (MatitaMisc.obj_file_of_script (find path)) + with + Sys_error _ -> + MatitaLog.error + ("In file " ^ file ^ " unable to include " ^ path) + ) + | _ -> () + with + CicNotationParser.Parse_error _ as exn -> + prerr_endline ("Unable to parse: " ^ file); + prerr_endline (MatitaExcPp.to_string exn); + () done with - | CicNotationParser.Parse_error _ as exn -> - prerr_endline ("Unable to parse: " ^ file); - prerr_endline (MatitaExcPp.to_string exn); - exit 1 | End_of_file -> close_in ic); Hashtbl.iter (fun file alias -> let dep = resolve alias in match dep with | None -> () - | Some d -> Hashtbl.add deps file d) - aliases) - !files; - List.iter (fun file -> + | Some u -> Hashtbl.add deps file (MatitaMisc.obj_file_of_baseuri u)) + aliases + ) !files; + List.iter + (fun file -> let deps = Hashtbl.find_all deps file in let deps = List.fast_sort Pervasives.compare deps in let deps = MatitaMisc.list_uniq deps in - let deps = - List.map (fun x -> Pcre.replace ~pat:"ma$" ~templ:"moo" x) deps - in let deps = file :: deps in - Printf.printf "%s: %s\n" (MatitaMisc.obj_file_of_script file) - (String.concat " " deps)) - !files + let moo = MatitaMisc.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 + ) !files ;; let _ = main () -