--- 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)
}