From ad4a4b9f76a987637943341ab8465ef9a8a202d6 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 5 Feb 2004 17:59:39 +0000
Subject: [PATCH] - added support for multiple choices - added pping of
 toplevel exceptions

---
 helm/gTopLevel/testlibrary.ml | 34 +++++++++++++++++++++++++---------
 1 file changed, 25 insertions(+), 9 deletions(-)

diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml
index 0d09eb0e3..681b9b362 100644
--- 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 "[   OK   ]";
-        ok := uri_str :: !ok
-      end else begin
-        print_endline "[ FAILED ]";
-        nok := uri_str :: !nok
-      end
+      match test_uri uri with
+      | `Ok ->
+          print_endline "[   OK   ]";
+          ok := uri_str :: !ok
+      | `Nok ->
+          print_endline "[ FAILED ]";
+          nok := uri_str :: !nok
+      | `Maybe ->
+          print_endline "[  MANY  ]";
+          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 ()
 
-- 
2.39.2