X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fprobe%2Fengine.ml;h=345f065fec977afc91fda19b548640d0cd5caf9c;hp=8a8a74ac545b644aedb95915d0271b222d764150;hb=ea99a55173ebdcfe60f3b3d6f6c979f5d7785d48;hpb=42fb6dce8110e29ccf233c09e6d6b1d58d9e5fef

diff --git a/matita/components/binaries/probe/engine.ml b/matita/components/binaries/probe/engine.ml
index 8a8a74ac5..345f065fe 100644
--- a/matita/components/binaries/probe/engine.ml
+++ b/matita/components/binaries/probe/engine.ml
@@ -19,47 +19,38 @@ 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))
+module X = Error
 
 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
-   US.iter map uris
+  let map uri = P.printf "%S\n" (U.string_of_uri uri) in
+  US.iter map uris
 
 let is_registry str =
-   F.check_suffix str ".conf.xml"
+  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
+    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 X.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 X.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 ich = open_in fname in
+  let lexbuf = Lexing.from_channel ich in
+  M.token lexbuf; close_in ich