2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
14 module R = Helm_registry
16 module B = NCicLibrary
17 module C = NCicTypeChecker
33 H.set_log_callback no_log
35 let scan_uri devel str =
36 M.from_string (R.get "matita.basedir") devel str;
40 let devel, uri = E.get_uri devel in
43 let set_g () = O.exclude := `Generated :: !O.exclude
45 let set_p () = O.exclude := `Provided :: !O.exclude
47 let out_i () = E.out_int !O.net
49 let out_on () = E.out_length !O.objs
51 let out_os () = E.out_uris !O.objs
53 let out_sn () = E.out_length !O.srcs
55 let out_ss () = E.out_uris !O.srcs
58 if L.is_uri s then scan_uri "" s
59 else if E.is_registry s then init s
63 let help = "Usage: probe [ -X | <configuration file> | -gp | HELM (base)uri | -i | -on | os | -sn | -ss ]*" in
64 let help_X = " Reset options and counters" in
65 let help_g = " Exclude generated objects" in
66 let help_i = " Print the total intrinsic size" in
67 let help_p = " Exclude provided objects" in
68 let help_on = " Print the number of objects" in
69 let help_os = " Print the list of objects" in
70 let help_sn = " Print the number of sources" in
71 let help_ss = " Print the list of sources" in
73 "-X" , A.Unit O.clear, help_X;
74 "-g" , A.Unit set_g, help_g;
75 "-i" , A.Unit out_i, help_i;
76 "-on", A.Unit out_on, help_on;
77 "-os", A.Unit out_os, help_os;
78 "-p" , A.Unit set_p, help_p;
79 "-sn", A.Unit out_sn, help_sn;
80 "-ss", A.Unit out_ss, help_ss;