- 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 lexer =
+ match !level with
+ "1" -> CicNotationLexer.level1_pattern_lexer
+ | "2@" -> CicNotationLexer.level2_ast_lexer
+ | "2$" -> CicNotationLexer.level2_meta_lexer
+ | l ->
+ prerr_endline (Printf.sprintf "Unsupported level %s" l);
+ exit 2
+ in
+ let token_stream =
+ fst (lexer.Token.tok_func (Obj.magic (Ulexing.from_utf8_channel !ic)))
+ in
+ Printf.printf "Lexing notation level %s\n" !level; flush stdout;