unified grammars and lexers in a single one

[helm.git] / helm / ocaml / cic_notation / test_lexer.ml

diff --git a/helm/ocaml/cic_notation/test_lexer.ml b/helm/ocaml/cic_notation/test_lexer.ml
index b41f7f6b8e34355f31d290840eb497b95fae9dba..386c0f1b98b19b21433e8169f9eacd67f0f7cfa4 100644 (file)
--- a/helm/ocaml/cic_notation/test_lexer.ml
+++ b/helm/ocaml/cic_notation/test_lexer.ml
@@ -26,19 +26,14 @@
 let _ =
   let level = ref ~-1 in
   let ic = ref stdin in
-  let arg_spec = [ "-level", Arg.Set_int level, "set the notation level" ] in
-  let usage = "test_lexer -level { 1 | 2 | 3 } [ file ]" in
+  let arg_spec = [] in
+  let usage = "test_lexer [ file ]" in
   let open_file fname =
     if !ic <> stdin then close_in !ic;
     ic := open_in fname
   in
   Arg.parse arg_spec open_file usage;
-  let lexer =
-    match !level with
-    | 1 -> CicNotationLexer.syntax_pattern_lexer
-    | 2 -> CicNotationLexer.ast_pattern_lexer
-    | _ -> Arg.usage arg_spec usage; exit 1
-  in
+  let lexer = CicNotationLexer.notation_lexer in
   let token_stream = fst (lexer.Token.tok_func (Stream.of_channel !ic)) in
   Printf.printf "Lexing notation level %d\n" !level; flush stdout;
   let rec dump () =