]> matita.cs.unibo.it Git - helm.git/blob - matita/components/binaries/probe/probe.ml
- nUri : added Sets of uris for use in "probe"
[helm.git] / matita / components / binaries / probe / probe.ml
1 (*
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.                     
5     ||I||                                                                
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_______________________________________________________________ *)
11
12 module A = Arg
13
14 module R = Helm_registry
15 module L = Librarian
16 module B = NCicLibrary
17 module C = NCicTypeChecker
18 module H = HLog
19
20 module O = Options
21 module M = MatitaList
22 module S = NCicScan
23 module E = Engine
24
25 let trusted _ = true
26
27 let no_log _ _ = ()
28
29 let init registry =
30    R.load_from registry; 
31    B.init (); 
32    C.set_trust trusted;
33    H.set_log_callback no_log
34
35 let scan_uri devel str =
36    M.from_string (R.get "matita.basedir") devel str;
37    S.scan ()
38
39 let scan_from devel =
40    let devel, uri = E.get_uri devel in
41    scan_uri devel uri
42
43 let set_g () = O.exclude := `Generated :: !O.exclude
44
45 let set_p () = O.exclude := `Provided :: !O.exclude
46
47 let out_i () = E.out_int !O.net
48
49 let out_on () = E.out_length !O.objs
50
51 let out_os () = E.out_uris !O.objs
52
53 let out_sn () = E.out_length !O.srcs 
54
55 let out_ss () = E.out_uris !O.srcs
56
57 let process s =
58    if L.is_uri s then scan_uri "" s
59    else if E.is_registry s then init s
60    else scan_from s
61
62 let _ =
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
72    A.parse [
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;
81    ] process help