# HG changeset patch
# User wenzelm
# Date 1399367773 -7200
# Node ID f7c793b7fe7d9d59217c68b60e3017d2703a5f62
# Parent  1435f0c771dcb0f8a050e48aba508798a5d2fd64
tuned;

diff -r 1435f0c771dc -r f7c793b7fe7d src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon May 05 22:14:56 2014 +0200
+++ b/src/Pure/Tools/build.scala	Tue May 06 11:16:13 2014 +0200
@@ -26,11 +26,12 @@
     def echo(msg: String) {}
     def theory(session: String, theory: String) {}
     def stopped: Boolean = false
+    override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
   }
 
   object Ignore_Progress extends Progress
 
-  class Console_Progress(verbose: Boolean) extends Progress
+  class Console_Progress(verbose: Boolean = false) extends Progress
   {
     override def echo(msg: String) { Console.println(msg) }
     override def theory(session: String, theory: String): Unit =
diff -r 1435f0c771dc -r f7c793b7fe7d src/Pure/Tools/build_doc.scala
--- a/src/Pure/Tools/build_doc.scala	Mon May 05 22:14:56 2014 +0200
+++ b/src/Pure/Tools/build_doc.scala	Tue May 06 11:16:13 2014 +0200
@@ -79,7 +79,7 @@
           Properties.Value.Boolean(system_mode) ::
           Command_Line.Chunks(docs) =>
             val options = Options.init()
-            val progress = new Build.Console_Progress(false)
+            val progress = new Build.Console_Progress()
             progress.interrupt_handler {
               build_doc(options, progress, all_docs, max_jobs, system_mode, docs)
             }