# HG changeset patch
# User wenzelm
# Date 1674246527 -3600
# Node ID c066335efd2ee788d0f7f2aaac26f252e9763b20
# Parent  02738f4333eecd4f94bceb2d679d7f2daad7b11d
clarified signature;

diff -r 02738f4333ee -r c066335efd2e src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Fri Jan 20 21:19:11 2023 +0100
+++ b/src/Pure/Thy/bibtex.scala	Fri Jan 20 21:28:47 2023 +0100
@@ -160,18 +160,18 @@
 
   /* entries */
 
+  sealed case class Entry(name: String, pos: Position.T) {
+    def encode: String = YXML.string_of_body(XML.Encode.properties(Markup.Name(name) ::: pos))
+  }
+
   object Entries {
-    sealed case class Item(name: String, pos: Position.T) {
-      def encode: String = YXML.string_of_body(XML.Encode.properties(Markup.Name(name) ::: pos))
-    }
-
     val empty: Entries = apply(Nil)
 
-    def apply(entries: List[Item], errors: List[String] = Nil): Entries =
+    def apply(entries: List[Entry], errors: List[String] = Nil): Entries =
       new Entries(entries, errors)
 
     def parse(text: String, start: Isar_Token.Pos = Isar_Token.Pos.start): Entries = {
-      val entries = new mutable.ListBuffer[Item]
+      val entries = new mutable.ListBuffer[Entry]
       var pos = start
       var err_line = 0
 
@@ -179,7 +179,7 @@
         for (chunk <- Bibtex.parse(text)) {
           val pos1 = pos.advance(chunk.source)
           if (chunk.name != "" && !chunk.is_command) {
-            entries += Item(chunk.name, pos.position(pos1.offset))
+            entries += Entry(chunk.name, pos.position(pos1.offset))
           }
           if (chunk.is_malformed && err_line == 0) { err_line = pos.line }
           pos = pos1
@@ -198,7 +198,7 @@
     }
   }
 
-  final class Entries private(val entries: List[Entries.Item], val errors: List[String]) {
+  final class Entries private(val entries: List[Entry], val errors: List[String]) {
     override def toString: String = "Bibtex.Entries(" + entries.length + ")"
 
     def ::: (other: Entries): Entries =