let _ =
- NCicTypeChecker.set_logger
+ let indent = ref 0 in
+ let do_indent () = String.make !indent ' ' in
+ NCicTypeChecker.set_logger
(function
- | `Start_type_checking s -> ()
-(* prerr_endline ("Start: " ^ NUri.string_of_uri s) *)
- | `Type_checking_completed s -> ()
-(* prerr_endline ("End: " ^ NUri.string_of_uri s) *)
+ | `Start_type_checking s -> ();
+(* prerr_endline (do_indent () ^ "Start: " ^ NUri.string_of_uri s);
+ incr indent
+*)
+ | `Type_checking_completed s -> ();
+(*
+ decr indent;
+ prerr_endline (do_indent () ^ "End: " ^ NUri.string_of_uri s)
+*)
);
NCicPp.set_ppterm NCicPp.trivial_pp_term;
Helm_registry.load_from "conf.xml";
let s = Sys.argv.(1) in
if s = "-alluris" then
begin
- let uri_re = Str.regexp ".*\\(ind\\|var\\|con\\)$" in
+ let uri_re = Str.regexp ".*\\(ind\\|con\\)$" in
let uris = Http_getter.getalluris () in
let alluris = List.filter (fun u -> Str.string_match uri_re u 0) uris in
let oc = open_out "alluris.txt" in
in
prerr_endline "caching objects";
List.iter (fun uu ->
+ indent := 0;
(* prerr_endline ("************* INIZIO **************** " ^ NUri.string_of_uri uu); *)
let _,o = NCicEnvironment.get_obj uu in
try
| NCicTypeChecker.AssertFailure s
| NCicTypeChecker.TypeCheckerFailure s as e ->
(* prerr_endline ("Obj: " ^ NCicPp.ppobj o); *)
- prerr_endline (Lazy.force s); raise e
+ prerr_endline ("######### " ^ Lazy.force s); raise e
| CicEnvironment.Object_not_found s ->
prerr_endline ("Obj not found: " ^ UriManager.string_of_uri s);
)
prerr_endline "typechecking, first with the new and then with the old kernel";
let prima = Unix.gettimeofday () in
List.iter
- (fun u -> NCicTypeChecker.typecheck_obj (snd (NCicEnvironment.get_obj u)))
+ (fun u ->
+ indent := 0;
+ NCicTypeChecker.typecheck_obj (snd (NCicEnvironment.get_obj u)))
alluris;
let dopo = Unix.gettimeofday () in
Gc.compact ();