From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 27 Mar 2006 11:28:06 +0000 (+0000)
Subject: More robust handling of Control-C.
X-Git-Tag: make_still_working~7459
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=35e2f71ae7a80947ea53282418034674c3538c32;p=helm.git

More robust handling of Control-C.
---

diff --git a/helm/software/components/binaries/utilities/test_library.ml b/helm/software/components/binaries/utilities/test_library.ml
index f0e9510db..57939da48 100644
--- a/helm/software/components/binaries/utilities/test_library.ml
+++ b/helm/software/components/binaries/utilities/test_library.ml
@@ -55,6 +55,8 @@ let urifname =
 
 let ic = open_in urifname
 
+exception Done;;
+
 let _ =
   try
     while true do
@@ -85,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;
@@ -99,4 +110,4 @@ let _ =
     done
   with
      End_of_file
-   | Sys.Break -> ()
+   | Done -> ()