X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_notation%2FcicNotationLexer.ml;h=3c262ceec1854c27a502b9c56f1d8853a04bd430;hb=76371b115479873c07d16a047978394ebd4d495e;hp=306cf45b915f88d324ebed695b90ec0caaeb367c;hpb=31d7f139796d6597915cd430baf37552dc26511c;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationLexer.ml b/helm/ocaml/cic_notation/cicNotationLexer.ml
index 306cf45b9..3c262ceec 100644
--- a/helm/ocaml/cic_notation/cicNotationLexer.ml
+++ b/helm/ocaml/cic_notation/cicNotationLexer.ml
@@ -35,11 +35,22 @@ let regexp ident = xml_letter ident_cont* ident_decoration*
 
 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 *)
+  ('.' ident)+                        (* ext *)
+  ("#xpointer(" number ('/' number)+ ")")?  (* xpointer *)
+
 let error lexbuf msg =
   let begin_cnum, end_cnum = Ulexing.loc lexbuf in
   raise (Error (begin_cnum, end_cnum, msg))
@@ -58,6 +69,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 =
@@ -91,32 +104,22 @@ 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+ -> level1_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