]> matita.cs.unibo.it Git - helm.git/commitdiff
'{' and '}' are now considered as blanks
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 19 Mar 2003 09:10:57 +0000 (09:10 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 19 Mar 2003 09:10:57 +0000 (09:10 +0000)
helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll

index d40f09fb29ab04338e9db53611bf9e17911fbc77..692a6a86b1f6e0a47e087e720c52d5b5cb4b0dfe 100644 (file)
@@ -57,7 +57,7 @@ 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' '~'] | "\\;"
+let blanks = [' ' '\t' '\n' '~' '{' '}'] | "\\;"
 rule token =
  parse
     blanks      { token lexbuf } (* skip blanks *)