# HG changeset patch
# User wenzelm
# Date 1412443591 -7200
# Node ID 299b82d12d530201bd65ed119294e520dd4f055d
# Parent  207fb06aa18970ae9a6072d3c188c579ab77cadd
proper treatment of @comment (amending 402a8e8107a7);

diff -r 207fb06aa189 -r 299b82d12d53 src/Pure/Tools/bibtex.scala
--- a/src/Pure/Tools/bibtex.scala	Sat Oct 04 18:26:25 2014 +0200
+++ b/src/Pure/Tools/bibtex.scala	Sat Oct 04 19:26:31 2014 +0200
@@ -333,13 +333,13 @@
     {
       ctxt match {
         case Ignored_Context =>
+          ignored_line |
           item_start ~ (left_brace | left_paren) ~ opt(item_name) ^^
             { case (kind, a) ~ b ~ c =>
                 val right = if (b.source == "{") "}" else ")"
                 val chunk = Chunk(kind, a ::: List(b) ::: (c getOrElse Nil))
                 (chunk, Item_Context(kind, Closed, right)) } |
-          recover_item ^^ { case a => (a, Ignored_Context) } |
-          ignored_line
+          recover_item ^^ { case a => (a, Ignored_Context) }
         case item_ctxt @ Item_Context(kind, delim, right) =>
           if (delim.depth > 0)
             delimited_line(item_ctxt) |