# HG changeset patch # User wenzelm # Date 1672175311 -3600 # Node ID fa70b536ec500865667ca1a8402891c6a56a4288 # Parent 23f433294173b2b089fe08d0d6f34fc7ddd1f9f8 tuned output; diff -r 23f433294173 -r fa70b536ec50 src/Pure/Thy/bibtex.scala --- a/src/Pure/Thy/bibtex.scala Tue Dec 27 17:35:01 2022 +0100 +++ b/src/Pure/Thy/bibtex.scala Tue Dec 27 22:08:31 2022 +0100 @@ -201,6 +201,8 @@ } final class Entries private(val entries: List[Text.Info[String]], val errors: List[String]) { + override def toString: String = "Bibtex.Entries(" + entries.length + ")" + def ::: (other: Entries): Entries = new Entries(entries ::: other.entries, errors ::: other.errors) } diff -r 23f433294173 -r fa70b536ec50 src/Pure/Thy/file_format.scala --- a/src/Pure/Thy/file_format.scala Tue Dec 27 17:35:01 2022 +0100 +++ b/src/Pure/Thy/file_format.scala Tue Dec 27 22:08:31 2022 +0100 @@ -8,7 +8,9 @@ object File_Format { - object No_Data extends AnyRef + object No_Data extends AnyRef { + override def toString: String = "File_Format.No_Data" + } sealed case class Theory_Context(name: Document.Node.Name, content: String)