# HG changeset patch
# User wenzelm
# Date 1495390272 -7200
# Node ID 29a31cf0b4bc0cd91a8bbda8eac0e9e0358fa466
# Parent  cc6fdf8d1dc28a09c8a49994558e9fab4ff83c7b
more Progress variations;

diff -r cc6fdf8d1dc2 -r 29a31cf0b4bc src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Sun May 21 18:06:05 2017 +0200
+++ b/src/Pure/System/progress.scala	Sun May 21 20:11:12 2017 +0200
@@ -54,3 +54,29 @@
     is_stopped
   }
 }
+
+class File_Progress(path: Path, verbose: Boolean = false) extends Progress
+{
+  override def echo(msg: String): Unit =
+    File.append(path, msg + "\n")
+
+  override def theory(session: String, theory: String): Unit =
+    if (verbose) echo(session + ": theory " + theory)
+
+  override def toString: String = path.toString
+}
+
+class Seq_Progress(progress1: Progress, progress2: Progress) extends Progress
+{
+  override def echo(msg: String)
+  {
+    progress1.echo(msg)
+    progress2.echo(msg)
+  }
+
+  override def theory(session: String, theory: String)
+  {
+    progress1.theory(session, theory)
+    progress2.theory(session, theory)
+  }
+}