clarified nesting of delimiters;
authorwenzelm
Sat, 04 Oct 2014 16:02:17 +0200
changeset 58532 af2fc25662b6
parent 58531 454962877285
child 58533 dfbfc92118eb
clarified nesting of delimiters;
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
           }