# HG changeset patch
# User wenzelm
# Date 1412612264 -7200
# Node ID 877c5ecee25311569f414220bb23d198e45a3d80
# Parent  127f192b755c19004e91220c55d5cf2b00fe8610
more total parser;

diff -r 127f192b755c -r 877c5ecee253 src/Pure/Tools/bibtex.scala
--- a/src/Pure/Tools/bibtex.scala	Mon Oct 06 18:11:16 2014 +0200
+++ b/src/Pure/Tools/bibtex.scala	Mon Oct 06 18:17:44 2014 +0200
@@ -361,6 +361,7 @@
         case Item_Start(kind) =>
           space ^^ { case a => (Chunk(kind, List(a)), ctxt) } |
           item_begin ^^ { case (end, a) => (Chunk(kind, List(a)), Item_Open(kind, end)) } |
+          recover_item ^^ { case a => (a, Ignored) } |
           ignored_line
 
         case Item_Open(kind, end) =>