X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationLexer.ml;h=3c262ceec1854c27a502b9c56f1d8853a04bd430;hb=5d5e328a05ed70fcf565aef8f92b7ec87b2740f2;hp=dfbedef733661e0ab2dc2aa4cdad6315004810e2;hpb=4a7dd5f16ad7a3ac176c0650580f736ae73f373d;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationLexer.ml b/helm/ocaml/cic_notation/cicNotationLexer.ml
index dfbedef73..3c262ceec 100644
--- a/helm/ocaml/cic_notation/cicNotationLexer.ml
+++ b/helm/ocaml/cic_notation/cicNotationLexer.ml
@@ -35,11 +35,16 @@ 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 *)
@@ -106,9 +111,12 @@ let rec token = lexer
   | 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 *)