--- a/src/Pure/Thy/bibtex.scala Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Thy/bibtex.scala Thu Mar 04 15:41:46 2021 +0100
@@ -389,7 +389,9 @@
def heading_length: Int =
if (name == "") 1
- else (0 /: tokens.takeWhile(tok => !tok.is_open)){ case (n, tok) => n + tok.source.length }
+ else {
+ tokens.takeWhile(tok => !tok.is_open).foldLeft(0) { case (n, tok) => n + tok.source.length }
+ }
def is_ignored: Boolean = kind == "" && tokens.forall(_.is_ignored)
def is_malformed: Boolean = kind == "" || tokens.exists(_.is_malformed)