X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fprobe%2Fengine.ml;h=0fe7ace5323168e188df2e54f62f68f961fb8eb1;hb=2f19651bcec24abfb1bf15ff7e1387daad1f6638;hp=55936e5423aa5b594eae1c1566c718bd261f87a3;hpb=243d091f23f8338e155cdde14969a6043b8c89af;p=helm.git

diff --git a/matita/components/binaries/probe/engine.ml b/matita/components/binaries/probe/engine.ml
index 55936e542..0fe7ace53 100644
--- a/matita/components/binaries/probe/engine.ml
+++ b/matita/components/binaries/probe/engine.ml
@@ -18,14 +18,16 @@ 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 =
-   failwith (P.sprintf "probe: missing root: %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
 
@@ -41,22 +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
-      | _      -> 
-         if bdir = F.current_dir_name || bdir = F.dir_sep then unrooted dir else
+      | 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 bpath = F.dirname str ^ "/" in
-   bpath, buri
-*)
+
+let mac fname =
+   let ich = open_in fname in
+   let lexbuf = Lexing.from_channel ich in
+   M.token lexbuf; close_in ich
+