[ ("->", <:unicode<to>>); ("=>", <:unicode<Rightarrow>>);
("<=", <:unicode<leq>>); (">=", <:unicode<geq>>);
("<>", <:unicode<neq>>); (":=", <:unicode<def>>);
+ ("==", <:unicode<equiv>>);
]
-let regexp uri_step = [ 'a' - 'z' 'A' - 'Z' '0' - '9' '_' '-' ]+
+let regexp uri_step = [ 'a' - 'z' 'A' - 'Z' '0' - '9' '_' '-' ''' ]+
let regexp uri =
("cic:/" | "theory:/") (* schema *)
and level2_ast_token =
lexer
| xml_blank+ -> ligatures_token level2_ast_token lexbuf
- | meta -> return lexbuf ("META", Ulexing.utf8_lexeme lexbuf)
+ | meta ->
+ let s = Ulexing.utf8_lexeme lexbuf in
+ return lexbuf ("META", String.sub s 1 (String.length s - 1))
| implicit -> return lexbuf ("IMPLICIT", "")
| placeholder -> return lexbuf ("PLACEHOLDER", "")
| ident ->