proper treatment of @comment (amending 402a8e8107a7);
authorwenzelm
Sat, 04 Oct 2014 19:26:31 +0200
changeset 58538 299b82d12d53
parent 58537 207fb06aa189
child 58539 b31af96b7f5b
proper treatment of @comment (amending 402a8e8107a7);
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) |