# HG changeset patch
# User wenzelm
# Date 1672070227 -3600
# Node ID caeb732db09f8f46f48c6157ead0d021f27a96d0
# Parent  4086a0e4723bd150772b04ad529bdcf06bcf77f1
more bibtex errors;
clarified Bibtex.Chunk.is_malformed (again): see also 9c1389befa56 and 7ee248f19ca9;

diff -r 4086a0e4723b -r caeb732db09f src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Mon Dec 26 16:44:13 2022 +0100
+++ b/src/Pure/Thy/bibtex.scala	Mon Dec 26 16:57:07 2022 +0100
@@ -160,9 +160,11 @@
     def apply(entries: List[Text.Info[String]], errors: List[String] = Nil): Entries =
       new Entries(entries, errors)
 
-    def parse(text: String): Entries = {
+    def parse(text: String, file_pos: String = ""): Entries = {
       val entries = new mutable.ListBuffer[Text.Info[String]]
       var offset = 0
+      var line = 1
+      var err_line = 0
 
       try {
         for (chunk <- Bibtex.parse(text)) {
@@ -170,9 +172,19 @@
           if (chunk.name != "" && !chunk.is_command) {
             entries += Text.Info(Text.Range(offset, end_offset), chunk.name)
           }
+          if (chunk.is_malformed && err_line == 0) { err_line = line }
           offset = end_offset
+          line += chunk.source.count(_ == '\n')
         }
-        apply(entries.toList)
+
+        val err_pos =
+          if (err_line == 0 || file_pos.isEmpty) Position.none
+          else Position.Line_File(err_line, file_pos)
+        val errors =
+          if (err_line == 0) Nil
+          else List("Malformed bibtex file" + Position.here(err_pos))
+
+        apply(entries.toList, errors = errors)
       }
       catch { case ERROR(msg) => apply(Nil, errors = List(msg)) }
     }
@@ -396,7 +408,7 @@
       }
 
     def is_ignored: Boolean = kind == "" && tokens.forall(_.is_ignored)
-    def is_malformed: Boolean = kind == "" || tokens.exists(_.is_malformed)
+    def is_malformed: Boolean = tokens.exists(_.is_malformed)
     def is_command: Boolean = Bibtex.is_command(kind) && name != "" && content.isDefined
     def is_entry: Boolean = Bibtex.is_entry(kind) && name != "" && content.isDefined
   }
diff -r 4086a0e4723b -r caeb732db09f src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Dec 26 16:44:13 2022 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Dec 26 16:57:07 2022 +0100
@@ -643,7 +643,7 @@
         if File.is_bib(file.file_name)
       } yield {
         val path = dir + document_dir + file
-        Bibtex.Entries.parse(File.read(path))
+        Bibtex.Entries.parse(File.read(path), file_pos = path.expand.implode)
       }).foldRight(Bibtex.Entries.empty)(_ ::: _)
 
     def record_proofs: Boolean = options.int("record_proofs") >= 2