New implementation of the proof-checker daemon: there is now

[helm.git] / helm / proofChecker / proofChecker.ml

diff --git a/helm/proofChecker/proofChecker.ml b/helm/proofChecker/proofChecker.ml
index 4dfcb70b303af82d07f6d454776695ef47c16afd..1c7245164147eb8227b4ffb1c86418a6a13cf867 100644 (file)
--- a/helm/proofChecker/proofChecker.ml
+++ b/helm/proofChecker/proofChecker.ml
@@ -24,21 +24,33 @@
  *)
 
 let main () =
- let uris = ref [] in
- Arg.parse []
-  (fun uri -> uris :=  uri :: !uris)
+ let usage_msg =
   "
-usage: proofChecker uri ...
+usage: proofChecker[.opt]
+The proof-checker reads from the stdin one URI at a time and proof-checks it.
 
-List of options:";
- uris := List.rev !uris;
-  List.iter
-   (function uri ->
-     try
-        CicTypeChecker.typecheck (UriManager.uri_of_string uri)
-     with
-       e -> print_newline () ; flush stdout ; raise e 
-   ) !uris
+List of options:"
+ in
+  Arg.parse []
+   (fun _ -> 
+     begin
+      prerr_string "Error: no options expected.\n" ;
+      Arg.usage [] usage_msg ;
+      exit (-1)
+     end
+  ) usage_msg ;
+  while true do
+   begin
+    try
+     CicTypeChecker.typecheck (UriManager.uri_of_string (read_line ()))
+    with
+     e ->
+      print_newline() ;
+      flush stdout ;
+      raise e
+   end ;
+   print_endline "END"
+  done
 ;;
 
 CicCooking.init() ;