X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fprobe%2Fengine.ml;h=0fe7ace5323168e188df2e54f62f68f961fb8eb1;hb=2f19651bcec24abfb1bf15ff7e1387daad1f6638;hp=e79f000f9e471ad61a6c983145f09b06a2107a65;hpb=cbbbc763dc971b43fe74f1d08b797de5d1dc4f17;p=helm.git diff --git a/matita/components/binaries/probe/engine.ml b/matita/components/binaries/probe/engine.ml index e79f000f9..0fe7ace53 100644 --- a/matita/components/binaries/probe/engine.ml +++ b/matita/components/binaries/probe/engine.ml @@ -9,15 +9,57 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +module F = Filename module L = List module P = Printf -module U = NUri +module U = NUri +module US = U.UriSet +module B = Librarian +module H = HExtlib + +module M = MacLexer + +let unsupported protocol = + failwith (P.sprintf "probe: unsupported protocol: %s" protocol) + +let missing path = + failwith (P.sprintf "probe: missing path: %s" path) + +let unrooted path roots = + failwith (P.sprintf "probe: missing root: %s (found roots: %u)" path (L.length roots)) + +let out_int i = P.printf "%u\n" i + +let out_length uris = out_int (US.cardinal uris) let out_uris uris = let map uri = P.printf "%s\n" (U.string_of_uri uri) in - L.iter map uris + US.iter map uris -let out_int i = P.printf "%u\n" i +let is_registry str = + F.check_suffix str ".conf.xml" + +let get_uri str = + let str = H.normalize_path str in + let dir, file = + if H.is_regular str && F.check_suffix str ".ma" + then F.dirname str, F.chop_extension (F.basename str) + else if H.is_dir str then str, "" + else missing str + in + let rec aux bdir file = match B.find_roots_in_dir bdir with + | [root] -> + let buri = L.assoc "baseuri" (B.load_root_file root) in + F.concat bdir file, F.concat buri file + | roots -> + if bdir = F.current_dir_name || bdir = F.dir_sep then unrooted dir roots else + aux (F.dirname bdir) (F.concat (F.basename bdir) file) + in + aux dir file + +let mac fname = + let ich = open_in fname in + let lexbuf = Lexing.from_channel ich in + M.token lexbuf; close_in ich -let out_length l = out_int (L.length l)