# HG changeset patch
# User wenzelm
# Date 1660312127 -7200
# Node ID 0a14663dffcccffc0efeda28fe0fca77f2acb33f
# Parent  affd69bad2d448eb315ec38f29ac571b1f4f6198
clarified output;

diff -r affd69bad2d4 -r 0a14663dffcc src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Fri Aug 12 15:40:38 2022 +0200
+++ b/src/Pure/Thy/document_build.scala	Fri Aug 12 15:48:47 2022 +0200
@@ -31,10 +31,12 @@
   }
 
   sealed case class Document_Input(name: String, sources: SHA1.Digest)
-  extends Document_Name
+  extends Document_Name { override def toString: String = name }
 
   sealed case class Document_Output(name: String, sources: SHA1.Digest, log_xz: Bytes, pdf: Bytes)
   extends Document_Name {
+    override def toString: String = name
+
     def log: String = log_xz.uncompress().text
     def log_lines: List[String] = split_lines(log)