# HG changeset patch
# User wenzelm
# Date 1412360382 -7200
# Node ID 4b190c76309754147cec22a33cfc90786bc2e143
# Parent  f05ccce3eca2b95b98bbb763afb5f4e365401d28
strict spaces for item_start: despite actual bibtex syntax, but in accordance to bibtex modes in Emacs and jEdit;

diff -r f05ccce3eca2 -r 4b190c763097 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)))