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

diff --git a/matita/components/binaries/probe/probe.ml b/matita/components/binaries/probe/probe.ml
index d118fdab2..897148e97 100644
--- a/matita/components/binaries/probe/probe.ml
+++ b/matita/components/binaries/probe/probe.ml
@@ -22,27 +22,32 @@ module M = MatitaList
 module D = MatitaRemove
 module S = NCicScan
 module E = Engine
+module X = Error
 
 let trusted _ = true
 
 let no_log _ _ = ()
 
 let init registry =
-   R.load_from registry;
-   if !O.no_init then begin
-      B.init ();
-      C.set_trust trusted;
-      H.set_log_callback no_log;
-      O.no_init := false;
-   end
+  R.load_from registry;
+  if !O.no_init then begin
+    B.init ();
+    C.set_trust trusted;
+    H.set_log_callback no_log;
+    O.no_init := false;
+  end
 
 let scan_uri devel str =
-   M.from_string (R.get "matita.basedir") devel str;
-   S.scan ()
+  try 
+    M.from_string (R.get "matita.basedir") devel str;
+    S.scan ()
+  with
+  | X.Error s ->
+    Printf.eprintf "probe: %s\n%!" s
 
 let scan_from devel =
-   let devel, uri = E.get_uri devel in
-   scan_uri devel uri
+  let devel, uri = E.get_uri devel in
+  scan_uri devel uri
 
 let set_g () = O.exclude := `Generated :: !O.exclude
 
@@ -71,45 +76,45 @@ let out_ss () = E.out_uris !O.srcs
 let out_b file = O.out_deps file
 
 let process s =
-   if L.is_uri s then scan_uri "" s
-   else if E.is_registry s then init s
-   else scan_from s
+  if L.is_uri s then scan_uri "" s
+  else if E.is_registry s then init s
+  else scan_from s
 
 let clear () =
-   D.objects (); O.clear ()
+  D.objects (); O.clear ()
 
 let _ =
-   let help = "Usage: probe [ -LX | <configuration file> | -gip | <HELM (base)uri> | -f | -oc | -on | -os | -sc | -sn | -ss  ]*" in
-   let help_L  = " Activate lexer debugging" in
-   let help_X  = " Clear configuration, options and counters" in
-   let help_b  = "<file>  Print backward object dependences in this file" in
-   let help_f  = " Print the number of objects grouped by flavour" in
-   let help_g  = " Exclude generated objects" in
-   let help_i  = " Exclude implied objects" in
-   let help_nn = " Print the number of names" in
-   let help_ns = " Print the list of names" in
-   let help_oc = " Print the total intrinsic complexity (objects)" in
-   let help_on = " Print the number of objects" in
-   let help_os = " Print the list of objects" in
-   let help_p  = " Exclude provided objects" in
-   let help_sc = " Print the total extrinsic complexity (sources)" in
-   let help_sn = " Print the number of sources" in
-   let help_ss = " Print the list of sources" in
-   A.parse [
-      "-L" , A.Set O.debug_lexer, help_L;
-      "-X" , A.Unit clear , help_X;
-      "-b" , A.String out_b , help_b;
-      "-f" , A.Unit out_f , help_f;
-      "-g" , A.Unit set_g , help_g;
-      "-i" , A.Unit set_i , help_i;
-      "-nn", A.Unit out_nn, help_nn;
-      "-ns", A.Unit out_ns, help_ns;
-      "-oc", A.Unit out_oc, help_oc;
-      "-on", A.Unit out_on, help_on;
-      "-os", A.Unit out_os, help_os;
-      "-p" , A.Unit set_p , help_p;
-      "-sc", A.Unit out_sc, help_sc;
-      "-sn", A.Unit out_sn, help_sn;
-      "-ss", A.Unit out_ss, help_ss;
-   ] process help;
-   D.objects ()
+  let help = "Usage: probe [ -LX | <configuration file> | -gip | <HELM (base)uri> | -f | -oc | -on | -os | -sc | -sn | -ss  ]*" in
+  let help_L  = " Activate lexer debugging" in
+  let help_X  = " Clear configuration, options and counters" in
+  let help_b  = "<file>  Print backward object dependences in this file" in
+  let help_f  = " Print the number of objects grouped by flavour" in
+  let help_g  = " Exclude generated objects" in
+  let help_i  = " Exclude implied objects" in
+  let help_nn = " Print the number of names" in
+  let help_ns = " Print the list of names" in
+  let help_oc = " Print the total intrinsic complexity (objects)" in
+  let help_on = " Print the number of objects" in
+  let help_os = " Print the list of objects" in
+  let help_p  = " Exclude provided objects" in
+  let help_sc = " Print the total extrinsic complexity (sources)" in
+  let help_sn = " Print the number of sources" in
+  let help_ss = " Print the list of sources" in
+  A.parse [
+    "-L" , A.Set O.debug_lexer, help_L;
+    "-X" , A.Unit clear , help_X;
+    "-b" , A.String out_b , help_b;
+    "-f" , A.Unit out_f , help_f;
+    "-g" , A.Unit set_g , help_g;
+    "-i" , A.Unit set_i , help_i;
+    "-nn", A.Unit out_nn, help_nn;
+    "-ns", A.Unit out_ns, help_ns;
+    "-oc", A.Unit out_oc, help_oc;
+    "-on", A.Unit out_on, help_on;
+    "-os", A.Unit out_os, help_os;
+    "-p" , A.Unit set_p , help_p;
+    "-sc", A.Unit out_sc, help_sc;
+    "-sn", A.Unit out_sn, help_sn;
+    "-ss", A.Unit out_ss, help_ss;
+  ] process help;
+  D.objects ()