From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 10 Feb 2004 14:06:51 +0000 (+0000)
Subject: - fixed final log reporting (that was broken by one of the previous commits)
X-Git-Tag: V_0_3_0~35
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=923b3910899f2afa1c74e1973d484d088a0251c8;p=helm.git

- fixed final log reporting (that was broken by one of the previous commits)
- CicCache ==> CicEnvironment
---

diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml
index 21173e9e5..7f23b2f12 100644
--- a/helm/gTopLevel/testlibrary.ml
+++ b/helm/gTopLevel/testlibrary.ml
@@ -33,7 +33,7 @@ module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks)
 let debug_print s = prerr_endline ("^^^^^^ " ^ s)
 
 let test_uri uri =
-  let obj = CicCache.get_obj uri in
+  let obj = CicEnvironment.get_obj uri in
   let (annobj, _, _, ids_to_inner_sorts, _, _, _) =
     Cic2acic.acic_object_of_cic_object ~eta_fix:false obj
   in
@@ -88,15 +88,15 @@ let test_uri uri =
         (Printexc.to_string exn));
       `Nok
 
-let report ok nok maybe =
+let report (ok,nok,maybe) =
   print_newline ();
   print_endline "TestLibrary report";
   print_endline "Succeeded URIs:";
-  List.iter (fun s -> print_endline ("\t" ^ s)) ok;
+  List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !ok);
   print_endline "Failed URIs:";
-  List.iter (fun s -> print_endline ("\t" ^ s)) nok;
+  List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !nok);
   print_endline "Multiple answers URIs:";
-  List.iter (fun s -> print_endline ("\t" ^ s)) maybe;
+  List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !maybe);
   print_newline ()
 
 let do_uri (ok, nok, maybe) uri =
@@ -116,14 +116,17 @@ let do_uri (ok, nok, maybe) uri =
 let do_file status fname =
   try
     let ic = open_in fname in
-    while true do
-      let line = input_line ic in
-      try
-        let uri = UriManager.uri_of_string line in
-        do_uri status uri
-      with UriManager.IllFormedUri _ ->
-        printf "Error parsing URI '%s', ignoring it" line
-    done
+    (try
+      while true do
+        let line = input_line ic in
+        try
+          let uri = UriManager.uri_of_string line in
+          do_uri status uri
+        with UriManager.IllFormedUri _ ->
+          printf "Error parsing URI '%s', ignoring it" line
+      done
+    with End_of_file ->
+     close_in ic)
   with exn ->
     printf "Error trying to access '%s' (%s), skipping the file\n%!"
       fname (Printexc.to_string exn)
@@ -154,5 +157,5 @@ let _ =
           do_file status name
         else
           printf "Don't know what to do with '%s', ignoring it\n%!" name)
-    names
-
+    names ;
+  report status