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