# HG changeset patch
# User wenzelm
# Date 1527356346 -7200
# Node ID 1e1877cb9b3ac2763914fab5a7ff2a766a353f9c
# Parent  f1f5ccc85b25c33a7e3050436e4ef2ab73d4380e
clarified output;

diff -r f1f5ccc85b25 -r 1e1877cb9b3a src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sat May 26 17:37:15 2018 +0200
+++ b/src/Pure/Thy/export.scala	Sat May 26 19:39:06 2018 +0200
@@ -193,7 +193,8 @@
     export_dir: Path,
     progress: Progress = No_Progress,
     export_list: Boolean = false,
-    export_patterns: List[String] = Nil)
+    export_patterns: List[String] = Nil,
+    export_prefix: String = "")
   {
     using(store.open_database(session_name))(db =>
     {
@@ -203,7 +204,7 @@
         // list
         if (export_list) {
           (for ((theory_name, name) <- export_names) yield compound_name(theory_name, name)).
-            sorted.foreach(Output.writeln(_, stdout = true))
+            sorted.foreach(progress.echo(_))
         }
 
         // export
@@ -220,7 +221,7 @@
             entry <- read_entry(db, session_name, theory_name, name)
           } {
             val path = export_dir + Path.basic(theory_name) + Path.explode(name)
-            progress.echo("exporting " + path)
+            progress.echo(export_prefix + "export " + path)
             Isabelle_System.mkdirs(path.dir)
             Bytes.write(path, entry.uncompressed(cache = store.xz_cache))
           }