]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_textual_parser/cicTextualLexer.mll
New CicTextualParser: it now returns (approximately) a couple
[helm.git] / helm / ocaml / cic_textual_parser / cicTextualLexer.mll
index 31878bfe6e83d68405f1759597f7d5ac5840d4d4..d9b353cd708164258ac4822074a09b7444f756a3 100644 (file)
  ;;
 }
 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")
+let conuri = baseuri "con"
+let varuri = baseuri "var"
 let indtyuri = baseuri "ind#1/" num
 let indconuri = baseuri "ind#1/" num "/" num
 let blanks = [' ' '\t' '\n']
@@ -68,6 +69,7 @@ rule token =
   | "Type"      { TYPE }
   | ident       { ID (L.lexeme lexbuf) }
   | conuri      { CONURI (U.uri_of_string ("cic:" ^ L.lexeme lexbuf)) }
+  | varuri      { VARURI (U.uri_of_string ("cic:" ^ L.lexeme lexbuf)) }
   | indtyuri    { INDTYURI (indtyuri_of_uri ("cic:" ^ L.lexeme lexbuf)) }
   | indconuri   { INDCONURI (indconuri_of_uri("cic:" ^ L.lexeme lexbuf)) }
   | num         { NUM (int_of_string (L.lexeme lexbuf)) }