let regexp tex_token = '\\' ident
+let regexp delim_begin = "\\["
+let regexp delim_end = "\\]"
+
let regexp keyword = '"' ident '"'
let regexp implicit = '?'
let regexp meta = implicit number
+let regexp csymbol = '\'' ident
+
let regexp uri =
("cic:/" | "theory:/") (* schema *)
ident ('/' ident)* (* path *)
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 =
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)
| number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf)
| keyword -> return lexbuf (keyword lexbuf)
+ | delim_begin -> return lexbuf ("DELIM", Ulexing.utf8_lexeme lexbuf)
+ | delim_end -> return lexbuf ("DELIM", Ulexing.utf8_lexeme lexbuf)
| tex_token -> return lexbuf (expand_macro lexbuf)
| uri -> return lexbuf ("URI", Ulexing.utf8_lexeme lexbuf)
| eof -> return lexbuf ("EOI", "")
+ | csymbol -> return lexbuf ("CSYMBOL", Ulexing.utf8_lexeme lexbuf)
| _ -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)
(* API implementation *)
-let syntax_pattern_lexer = mk_lexer level1_token
-let ast_pattern_lexer = mk_lexer level2_token
+let notation_lexer = mk_lexer token