]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/binaries/probe/probe.ml
updated probe and matitadep
[helm.git] / matita / components / binaries / probe / probe.ml
index 16a2ce9e248921af4ca8aa217d1a39953d23e69e..94c8707a7b5ec7471f91cf18b7f377ee932bf955 100644 (file)
@@ -28,9 +28,9 @@ let trusted _ = true
 let no_log _ _ = ()
 
 let init registry =
-   R.load_from registry; 
+   R.load_from registry;
    if !O.no_init then begin
-      B.init (); 
+      B.init ();
       C.set_trust trusted;
       H.set_log_callback no_log;
       O.no_init := false;
@@ -64,18 +64,21 @@ let out_sn () = E.out_length !O.srcs
 
 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
 
-let clear () = 
+let 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
@@ -89,13 +92,14 @@ let _ =
    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;
       "-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;      
+      "-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;