--- 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 =