clarified output;
authorwenzelm
Sat, 26 May 2018 19:39:06 +0200
changeset 68291 1e1877cb9b3a
parent 68290 f1f5ccc85b25
child 68292 7ca0c23179e6
clarified output;
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))
           }