X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2Flibrarian.ml;h=919edb36c4f9104eb88ec5be974016b12637533c;hb=08e9d02504942642a917c0d3e4b4795e65172d89;hp=bab6dd2bc290a66f126e442352b580843b6da24c;hpb=02a3fa8f07e5bb99653fcf6211e39130c27c7a98;p=helm.git diff --git a/helm/software/components/library/librarian.ml b/helm/software/components/library/librarian.ml index bab6dd2bc..919edb36c 100644 --- a/helm/software/components/library/librarian.ml +++ b/helm/software/components/library/librarian.ml @@ -40,7 +40,10 @@ let remove_trailing_slash s = let load_root_file rootpath = let data = HExtlib.input_file rootpath in let lines = Str.split (Str.regexp "\n") data in - let clean s = Pcre.replace ~pat:"^ *" (Pcre.replace ~pat:" *$" s) in + let clean s = + Pcre.replace ~pat:"[ \t]+" ~templ:" " + (Pcre.replace ~pat:"^ *" (Pcre.replace ~pat:" *$" s)) + in List.map (fun l -> match Str.split (Str.regexp "=") l with @@ -79,6 +82,16 @@ let find_root_for ~include_paths file = raise (NoRootFor file) ;; +let mk_baseuri root extra = + let chop name = + assert(Filename.check_suffix name ".ma" || + Filename.check_suffix name ".mma"); + try Filename.chop_extension name + with Invalid_argument "Filename.chop_extension" -> name + in + remove_trailing_slash (HExtlib.normalize_path (root ^ "/" ^ chop extra)) +;; + let baseuri_of_script ~include_paths file = let root, buri, path = find_root_for ~include_paths file in let path = HExtlib.normalize_path path in @@ -92,16 +105,9 @@ let baseuri_of_script ~include_paths file = | _ -> raise (NoRootFor (file ^" "^path^" "^root)) in let extra_buri = substract lpath lroot in - let chop name = - assert(Filename.check_suffix name ".ma" || - Filename.check_suffix name ".mma"); - try Filename.chop_extension name - with Invalid_argument "Filename.chop_extension" -> name - in let extra = String.concat "/" extra_buri in root, - remove_trailing_slash (HExtlib.normalize_path - (buri ^ "/" ^ chop extra)), + mk_baseuri buri extra, path, extra ;; @@ -146,6 +152,7 @@ module type Format = options -> source_object -> string option * target_object val mtime_of_source_object: source_object -> float option val mtime_of_target_object: target_object -> float option + val is_readonly_buri_of: options -> source_object -> bool end module Make = functor (F:Format) -> struct @@ -283,17 +290,28 @@ module Make = functor (F:Format) -> struct purge_unwanted_roots wanted (newroots @ rest) ;; + let is_not_ro (opts,_,_) (f,_,r,_) = + match r with + | Some root -> not (F.is_readonly_buri_of opts f) + | None -> assert false + ;; + let rec make_aux root (lo,_,ct as opts) compiled failed deps = let todo = List.filter (is_buildable opts compiled deps) deps in let todo = List.filter (fun (f,_,_,_)->not (List.mem f failed)) todo in + let todo = + let local, remote = + List.partition (fun (_,_,froot,_) -> froot = Some root) todo + in + let local, skipped = List.partition (is_not_ro opts) local in + List.iter + (fun x -> + HLog.warn("Read only baseuri for: "^F.string_of_source_object(fst4 x))) + skipped; + remote @ local + in if todo <> [] then let compiled, failed = - let todo = - let local, remote = - List.partition (fun (_,_,froot,_) -> froot = Some root) todo - in - remote @ local - in List.fold_left (fun (c,f) (file,_,froot,tgt) -> let rc = @@ -337,7 +355,8 @@ module Make = functor (F:Format) -> struct if targets = [] then make_aux root opts [] [] deps else - make_aux root opts [] [] (purge_unwanted_roots targets deps) + make_aux root opts [] [] + (purge_unwanted_roots targets deps) in HLog.debug ("Leaving directory '"^root^"'"); Sys.chdir old_root; @@ -346,12 +365,19 @@ module Make = functor (F:Format) -> struct end -let write_deps_file root deps = - let oc = open_out (root ^ "/depends") in - List.iter - (fun (t,d) -> output_string oc (t^" "^String.concat " " d^"\n")) - deps; - close_out oc; - HLog.message ("Generated: " ^ root ^ "/depends") -;; - +let write_deps_file where deps = match where with + | Some root -> + let oc = open_out (root ^ "/depends") in + let map (t, d) = output_string oc (t^" "^String.concat " " d^"\n") in + List.iter map deps; close_out oc; + HLog.message ("Generated: " ^ root ^ "/depends") + | None -> + print_endline (String.concat " " (List.flatten (List.map snd deps))) + +(* FG ***********************************************************************) + +(* scheme uri part as defined in URI Generic Syntax (RFC 3986) *) +let uri_scheme_rex = Pcre.regexp "^[[:alpha:]][[:alnum:]\-+.]*:" + +let is_uri str = + Pcre.pmatch ~rex:uri_scheme_rex str