# HG changeset patch
# User wenzelm
# Date 1547202916 -3600
# Node ID aaa0b5f571e83044fdeaf39880e46cf5c79c939d
# Parent  e1188d9d616b608aa1e201d663de4cae9efd648a
clarified output;

diff -r e1188d9d616b -r aaa0b5f571e8 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Fri Jan 11 11:28:04 2019 +0100
+++ b/src/Pure/Thy/export.scala	Fri Jan 11 11:35:16 2019 +0100
@@ -73,7 +73,9 @@
     name: String,
     body: Future[(Boolean, Bytes)])
   {
-    override def toString: String = compound_name(theory_name, name)
+    override def toString: String = uncompressed().toString
+
+    def text: String = uncompressed().text
 
     def uncompressed(cache: XZ.Cache = XZ.cache()): Bytes =
     {