]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_textual_parser/cicTextualLexer.mll
Initial revision
[helm.git] / helm / ocaml / cic_textual_parser / cicTextualLexer.mll
index 8c1a5b4aed55f0067a0a337d89690a17f08a2404..1be084795a11505eb80764da93da88e1ad79d5b6 100644 (file)
@@ -49,7 +49,7 @@
  ;;
 }
 let num = ['1'-'9']['0'-'9']* | '0'
-let alfa = ['A'-'Z' 'a'-'z' '_']
+let alfa = ['A'-'Z' 'a'-'z' '_' ''' '-']
 let ident = alfa (alfa | num)*
 let baseuri = '/'(ident '/')* ident '.'
 let conuri = baseuri ("con" | "var")
@@ -80,6 +80,8 @@ rule token =
   | '?'         { IMPLICIT }
   | '('         { LPAREN }
   | ')'         { RPAREN }
+  | '['         { LBRACKET }
+  | ']'         { RBRACKET }
   | '{'         { LCURLY }
   | '}'         { RCURLY }
   | ';'         { SEMICOLON }
@@ -88,5 +90,6 @@ rule token =
   | ':'         { COLON }
   | '.'         { DOT }
   | "->"        { ARROW }
+  | "_"         { NONE }
   | eof         { EOF }
 {}