# HG changeset patch
# User wenzelm
# Date 1412431337 -7200
# Node ID af2fc25662b606aa131eb34b3e6d2249c1758d15
# Parent  454962877285a493432e9bf36f89b9b68f983b7b
clarified nesting of delimiters;

diff -r 454962877285 -r af2fc25662b6 src/Pure/Tools/bibtex.scala
--- a/src/Pure/Tools/bibtex.scala	Sat Oct 04 15:34:25 2014 +0200
+++ b/src/Pure/Tools/bibtex.scala	Sat Oct 04 16:02:17 2014 +0200
@@ -232,9 +232,13 @@
           while (!finished && i < end) {
             val c = in.source.charAt(i)
             if (c == '"' && d == 0) { i += 1; d = 1; q = true }
-            else if (c == '"' && d == 1) { i += 1; d = 0; q = false; finished = true }
+            else if (c == '"' && d == 1 && q) {
+              i += 1; d = 0; q = false; finished = true
+            }
             else if (c == '{') { i += 1; d += 1 }
-            else if (c == '}' && d > 0) { i += 1; d -= 1; if (d == 0) finished = true }
+            else if (c == '}' && (d > 1 || d == 1 && !q)) {
+              i += 1; d -= 1; if (d == 0) finished = true
+            }
             else if (d > 0) i += 1
             else finished = true
           }