This commit was manufactured by cvs2svn to create tag

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

diff --git a/helm/ocaml/cic_notation/cicNotationLexer.ml b/helm/ocaml/cic_notation/cicNotationLexer.ml
index 9721ee80503e22af6e4499a334ed6e8cf312784a..dfbedef733661e0ab2dc2aa4cdad6315004810e2 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationLexer.ml
+++ b/helm/ocaml/cic_notation/cicNotationLexer.ml
@@ -64,6 +64,8 @@ let return lexbuf token =
   let flocation_end = { flocation_begin with Lexing.pos_cnum = end_cnum } in
   (token, (flocation_begin, flocation_end))
 
+let return_lexeme lexbuf name = return lexbuf (name, Ulexing.utf8_lexeme lexbuf)
+
 let remove_quotes s = String.sub s 1 (String.length s - 2)
 
 let mk_lexer token =
@@ -97,21 +99,8 @@ let expand_macro lexbuf =
 
 let keyword lexbuf = "KEYWORD", remove_quotes (Ulexing.utf8_lexeme lexbuf)
 
-(** {2 Level 1 lexer} *)
-
-let rec level1_token = lexer
-  | xml_blank+ -> level1_token lexbuf
-  | ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf)
-  | number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf)
-  | keyword -> return lexbuf (keyword lexbuf)
-  | tex_token -> return lexbuf (expand_macro lexbuf)
-  | eof -> return lexbuf ("EOI", "")
-  | _ -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)
-
-(** {2 Level 2 lexer} *)
-
-let rec level2_token = lexer
-  | xml_blank+ -> level2_token lexbuf
+let rec token = lexer
+  | xml_blank+ -> token lexbuf
   | meta -> return lexbuf ("META", Ulexing.utf8_lexeme lexbuf)
   | implicit -> return lexbuf ("IMPLICIT", Ulexing.utf8_lexeme lexbuf)
   | ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf)
@@ -124,6 +113,5 @@ let rec level2_token = lexer
 
 (* API implementation *)
 
-let syntax_pattern_lexer = mk_lexer level1_token
-let ast_pattern_lexer = mk_lexer level2_token
+let notation_lexer = mk_lexer token