tuned;
authorwenzelm
Tue May 06 11:16:13 2014 +0200 (2014-05-06)
changeset 56873f7c793b7fe7d
parent 56872 1435f0c771dc
child 56874 5d78bce4f5a4
tuned;
src/Pure/Tools/build.scala
src/Pure/Tools/build_doc.scala
     1.1 --- a/src/Pure/Tools/build.scala	Mon May 05 22:14:56 2014 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Tue May 06 11:16:13 2014 +0200
     1.3 @@ -26,11 +26,12 @@
     1.4      def echo(msg: String) {}
     1.5      def theory(session: String, theory: String) {}
     1.6      def stopped: Boolean = false
     1.7 +    override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
     1.8    }
     1.9  
    1.10    object Ignore_Progress extends Progress
    1.11  
    1.12 -  class Console_Progress(verbose: Boolean) extends Progress
    1.13 +  class Console_Progress(verbose: Boolean = false) extends Progress
    1.14    {
    1.15      override def echo(msg: String) { Console.println(msg) }
    1.16      override def theory(session: String, theory: String): Unit =
     2.1 --- a/src/Pure/Tools/build_doc.scala	Mon May 05 22:14:56 2014 +0200
     2.2 +++ b/src/Pure/Tools/build_doc.scala	Tue May 06 11:16:13 2014 +0200
     2.3 @@ -79,7 +79,7 @@
     2.4            Properties.Value.Boolean(system_mode) ::
     2.5            Command_Line.Chunks(docs) =>
     2.6              val options = Options.init()
     2.7 -            val progress = new Build.Console_Progress(false)
     2.8 +            val progress = new Build.Console_Progress()
     2.9              progress.interrupt_handler {
    2.10                build_doc(options, progress, all_docs, max_jobs, system_mode, docs)
    2.11              }