X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fprobe%2Fengine.ml;h=0fe7ace5323168e188df2e54f62f68f961fb8eb1;hb=2f19651bcec24abfb1bf15ff7e1387daad1f6638;hp=c959e648c5e86af39229145ac6c76105bf0d9111;hpb=ebc170efe71cf4ee842acfbe58bb6864e76ba98c;p=helm.git diff --git a/matita/components/binaries/probe/engine.ml b/matita/components/binaries/probe/engine.ml index c959e648c..0fe7ace53 100644 --- a/matita/components/binaries/probe/engine.ml +++ b/matita/components/binaries/probe/engine.ml @@ -18,6 +18,8 @@ module US = U.UriSet module B = Librarian module H = HExtlib +module M = MacLexer + let unsupported protocol = failwith (P.sprintf "probe: unsupported protocol: %s" protocol) @@ -41,17 +43,23 @@ let is_registry str = let get_uri str = let str = H.normalize_path str in let dir, file = - if H.is_regular str && F.check_suffix str ".ma" + 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 + | [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 +