- added support for multiple choices

- added pping of toplevel exceptions

diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml
index 0d09eb0e3704de85f942b8fd5f0ecde7b47a6f5b..681b9b36275bccad0cdb67790f6abb2f75d17a98 100644 (file)
--- a/helm/gTopLevel/testlibrary.ml
+++ b/helm/gTopLevel/testlibrary.ml
@@ -8,6 +8,7 @@ let mqi_handle = MQIConn.init mqi_flags mqi_debug_fun
 let verbose = false
 
 exception Failure of string
+exception Multiple_interpretations
 let fail msg = raise (Failure msg)
 
 module DisambiguateCallbacks =
@@ -22,7 +23,7 @@ module DisambiguateCallbacks =
      List.filter
       (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
 
-  let interactive_interpretation_choice _ = fail "Multiple interpretations"
+  let interactive_interpretation_choice _ = raise Multiple_interpretations
   let input_or_locate_uri ~title = fail "Unknown identifier"
  end
 
@@ -75,12 +76,22 @@ let test_uri uri =
   | Cic.AInductiveDefinition _ ->
       debug_print "AInductiveDefinition: boh ..."
 
-let test_uri uri = try test_uri uri; true with _ -> false
+let test_uri uri =
+  try
+    test_uri uri;
+    `Ok
+  with
+  | Multiple_interpretations -> `Maybe
+  | exn ->
+      prerr_endline (sprintf "Top Level Uncaught Exception: %s"
+        (Printexc.to_string exn));
+      `Nok
 
 let _ =
   let idx = ref 0 in
   let ok = ref [] in
   let nok = ref [] in
+  let maybe = ref [] in
   try
     let mode = if Sys.argv.(1) = "-" then `Stdin else `Cmdline in
     while true do
@@ -92,13 +103,16 @@ let _ =
       in
       printf "Testing URI: %-55s " (uri_str ^ " ..."); flush stdout;
       let uri = UriManager.uri_of_string uri_str in
-      if test_uri uri then begin
-        print_endline "\e[01;32m[   OK   ]\e[00m";
-        ok := uri_str :: !ok
-      end else begin
-        print_endline "\e[01;31m[ FAILED ]\e[00m";
-        nok := uri_str :: !nok
-      end
+      match test_uri uri with
+      | `Ok ->
+          print_endline "\e[01;32m[   OK   ]\e[00m";
+          ok := uri_str :: !ok
+      | `Nok ->
+          print_endline "\e[01;31m[ FAILED ]\e[00m";
+          nok := uri_str :: !nok
+      | `Maybe ->
+          print_endline "\e[01;33m[  MANY  ]\e[00m";
+          maybe := uri_str :: !maybe
     done
   with Invalid_argument _ | End_of_file ->
     print_newline ();
@@ -107,5 +121,7 @@ let _ =
     List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !ok);
     print_endline "Failed URIs:";
     List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !nok);
+    print_endline "Multiple answers URIs:";
+    List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !maybe);
     print_newline ()