X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fbinaries%2Futilities%2Ftest_library.ml;h=57939da48c319bba1e506720f47f849ed08a5530;hb=bee84153d00d1e3d59c3a0a5ba0ab4cae773cf9e;hp=1947919aedca4896af2c7893c3b12f926141098c;hpb=46ef6e13c0833a5df3ae5f15b5641822454a8c9b;p=helm.git

diff --git a/components/binaries/utilities/test_library.ml b/components/binaries/utilities/test_library.ml
index 1947919ae..57939da48 100644
--- a/components/binaries/utilities/test_library.ml
+++ b/components/binaries/utilities/test_library.ml
@@ -43,7 +43,7 @@ let _ =
     Printf.printf "%s\n" separator;
     Printf.printf "Total: %.2f\n" !new_total;
     if !old_total <> 0.0 then
-     Printf.printf "Old: %.2f (%.2f)\n" !old_total (perc !new_total !old_total))
+     Printf.printf "Old: %.2f (%.2f%%)\n" !old_total (perc !new_total !old_total))
 ;;
 
 let urifname =
@@ -55,6 +55,8 @@ let urifname =
 
 let ic = open_in urifname
 
+exception Done;;
+
 let _ =
   try
     while true do
@@ -64,10 +66,12 @@ let _ =
         let uri,res,time =
          match Str.split (Str.regexp " ") uri with
             uri::res::time::_ -> uri, Some res, Some (float_of_string time)
+          | [uri;res] -> uri, Some res, None
           | [ uri ] -> uri, None, None
           | _ -> 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);
@@ -83,13 +87,22 @@ 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;
@@ -97,4 +110,4 @@ let _ =
     done
   with
      End_of_file
-   | Sys.Break -> ()
+   | Done -> ()