X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Futilities%2Ftest_library.ml;h=03742ac308a7efc02d68b929158fc5846e169f55;hb=dd1a439747a9f4448dc1cc845bfa6110db5ade41;hp=8abf5e9beaa28afa15d59c6624afd8a1b520d749;hpb=61a30c31ff641754b05928bab997001d1c90c593;p=helm.git

diff --git a/helm/software/components/binaries/utilities/test_library.ml b/helm/software/components/binaries/utilities/test_library.ml
index 8abf5e9be..03742ac30 100644
--- a/helm/software/components/binaries/utilities/test_library.ml
+++ b/helm/software/components/binaries/utilities/test_library.ml
@@ -23,7 +23,7 @@
  * http://helm.cs.unibo.it/
  *)
 
-let trust = false
+let trust = true
 let conffile = "../../../matita/matita.conf.xml"
 
 let _ = CicEnvironment.set_trust (fun _ -> trust);;
@@ -55,6 +55,8 @@ let urifname =
 
 let ic = open_in urifname
 
+exception Done;;
+
 let _ =
   try
     while true do
@@ -69,6 +71,7 @@ let _ =
           | _ -> assert false
         in
         Printf.printf "%s " uri;
+        flush stdout;
         let uri = UriManager.uri_of_string uri in
         let before = Unix.gettimeofday () in
         ignore (CicTypeChecker.typecheck uri);
@@ -84,18 +87,33 @@ let _ =
       with
         | End_of_file as exn -> raise exn
         | Sys.Break ->
-           Printf.printf "SKIPPED\n";
-           flush stdout;
-           Printf.eprintf "Continue with next URI? [y/_]";
-           flush stderr;
-           (match input_line stdin with
-               "y" -> ()
-             | _ -> raise Sys.Break)
+           let rec skip_break prompt =
+            try
+             if prompt then
+              begin
+               Printf.printf "SKIPPED\n";
+               flush stdout;
+               Printf.eprintf "Continue with next URI? [y/_]";
+               flush stderr;
+              end;
+             (match input_line stdin with
+                 "y" -> ()
+               | _ -> raise Done)
+            with
+             Sys.Break -> skip_break false
+           in
+            skip_break true
         | exn ->
            Printf.printf "FAIL\n";
            flush stdout;
-           prerr_endline (Printexc.to_string exn)
+           prerr_endline
+            (match exn with
+                CicTypeChecker.TypeCheckerFailure msg ->
+                 "TypeCheckerFailure: " ^ Lazy.force msg
+              | CicTypeChecker.AssertFailure msg ->
+                 "TypeCheckerAssertion: " ^ Lazy.force msg
+              | _ -> Printexc.to_string exn)
     done
   with
      End_of_file
-   | Sys.Break -> ()
+   | Done -> ()