tuned output;
authorwenzelm
Tue, 28 Aug 2018 12:42:57 +0200
changeset 68832 9b9fc9ea9dd1
parent 68831 a6c69599ab99
child 68834 43334463428a
child 68835 2e59da922630
tuned output;
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
       }
   }