tuned;
authorwenzelm
Tue, 06 May 2014 11:16:13 +0200
changeset 56873 f7c793b7fe7d
parent 56872 1435f0c771dc
child 56874 5d78bce4f5a4
tuned;
src/Pure/Tools/build.scala
src/Pure/Tools/build_doc.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 =
--- 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)
             }