strict spaces for item_start: despite actual bibtex syntax, but in accordance to bibtex modes in Emacs and jEdit;
authorwenzelm
Fri, 03 Oct 2014 20:19:42 +0200
changeset 58527 4b190c763097
parent 58526 f05ccce3eca2
child 58528 7d6b8f8893e8
strict spaces for item_start: despite actual bibtex syntax, but in accordance to bibtex modes in Emacs and jEdit;
src/Pure/Tools/bibtex.scala
--- a/src/Pure/Tools/bibtex.scala	Fri Oct 03 14:46:26 2014 +0200
+++ b/src/Pure/Tools/bibtex.scala	Fri Oct 03 20:19:42 2014 +0200
@@ -178,7 +178,7 @@
     override val whiteSpace = "".r
 
     private val space = """[ \t\n\r]+""".r ^^ token(Token.Kind.SPACE)
-    private val spaces = rep(space)
+    private val strict_space = """[ \t]+""".r ^^ token(Token.Kind.SPACE)
 
     private val ignored =
       rep1("""(?mi)([^@]+|@[ \t\n\r]*comment)""".r) ^^ { case ss => Ignored(ss.mkString) }
@@ -252,7 +252,7 @@
     /* chunks */
 
     private val item_start =
-      at ~ spaces ~ ident ~ spaces ^^
+      at ~ rep(strict_space) ~ ident ~ rep(strict_space) ^^
         { case a ~ b ~ c ~ d => List(a) ::: b ::: List(c) ::: d }
 
     private val body_token = delimited_token | ("[=#,]".r ^^ keyword | (nat | (ident | space)))