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
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
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 ()