# HG changeset patch
# User wenzelm
# Date 1535452977 -7200
# Node ID 9b9fc9ea9dd1624bd95a6748b520eee1934b57e7
# Parent  a6c69599ab99906f16413cb4492366246e90ebf5
tuned output;

diff -r a6c69599ab99 -r 9b9fc9ea9dd1 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Tue Aug 28 12:39:37 2018 +0200
+++ b/src/Pure/Thy/export.scala	Tue Aug 28 12:42:57 2018 +0200
@@ -203,18 +203,24 @@
       new Provider {
         def apply(export_name: String): Option[Entry] =
           read_entry(db, session_name, theory_name, export_name)
+
+        override def toString: String = db.toString
       }
 
     def snapshot(snapshot: Document.Snapshot): Provider =
       new Provider {
         def apply(export_name: String): Option[Entry] =
           snapshot.exports_map.get(export_name)
+
+        override def toString: String = snapshot.toString
       }
 
     def directory(dir: Path, session_name: String, theory_name: String): Provider =
       new Provider {
         def apply(export_name: String): Option[Entry] =
           read_entry(dir, session_name, theory_name, export_name)
+
+        override def toString: String = dir.toString
       }
   }