(debut) de grammaire minicoq

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@41 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 16 insertions, 1 deletions

diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index e4b1496a3a..79be85fadc 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -23,4 +23,19 @@ let rec globalize bv = function
   | Rel _ | DOP0 _ as c -> c
 
 let main () =
-  failwith "todo"
+  let cs = Stream.of_channel stdin in
+  while true do
+    try
+      let c = Grammar.Entry.parse G_minicoq.command cs in
+      Printf.printf "ok\n"; flush stdout
+    with 
+      | End_of_file | Stdpp.Exc_located (_, End_of_file) -> 
+	  exit 0
+      | Stdpp.Exc_located (_,e) ->
+	  Printf.printf "error: %s\n" (Printexc.to_string e); flush stdout
+      | exn -> 
+	  Printf.printf "error: %s\n" (Printexc.to_string exn); flush stdout
+  done
+
+let _ = Printexc.catch main ()
+