tuned;
authorwenzelm
Sat Oct 08 21:31:56 2016 +0200 (2016-10-08)
changeset 6411568619fa37ca7
parent 64114 45e065eea984
child 64116 6cfd429a4296
tuned;
src/Pure/PIDE/batch_session.scala
src/Pure/Tools/build.scala
src/Pure/Tools/ci_profile.scala
src/Pure/Tools/ml_console.scala
     1.1 --- a/src/Pure/PIDE/batch_session.scala	Sat Oct 08 14:09:55 2016 +0200
     1.2 +++ b/src/Pure/PIDE/batch_session.scala	Sat Oct 08 21:31:56 2016 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4      val parent_session =
     1.5        session_info.parent getOrElse error("No parent session for " + quote(session))
     1.6  
     1.7 -    if (!Build.build(options, new Console_Progress(verbose),
     1.8 +    if (!Build.build(options, new Console_Progress(verbose = verbose),
     1.9          verbose = verbose, build_heap = true,
    1.10          dirs = dirs, sessions = List(parent_session)).ok)
    1.11        new RuntimeException
    1.12 @@ -35,7 +35,7 @@
    1.13        new Resources(content.loaded_theories, content.known_theories, content.syntax)
    1.14      }
    1.15  
    1.16 -    val progress = new Console_Progress(verbose)
    1.17 +    val progress = new Console_Progress(verbose = verbose)
    1.18  
    1.19      val prover_session = new Session(resources)
    1.20      val batch_session = new Batch_Session(prover_session)
     2.1 --- a/src/Pure/Tools/build.scala	Sat Oct 08 14:09:55 2016 +0200
     2.2 +++ b/src/Pure/Tools/build.scala	Sat Oct 08 21:31:56 2016 +0200
     2.3 @@ -750,7 +750,7 @@
     2.4  
     2.5      val sessions = getopts(args)
     2.6  
     2.7 -    val progress = new Console_Progress(verbose)
     2.8 +    val progress = new Console_Progress(verbose = verbose)
     2.9  
    2.10      if (verbose) {
    2.11        progress.echo(
     3.1 --- a/src/Pure/Tools/ci_profile.scala	Sat Oct 08 14:09:55 2016 +0200
     3.2 +++ b/src/Pure/Tools/ci_profile.scala	Sat Oct 08 21:31:56 2016 +0200
     3.3 @@ -16,7 +16,7 @@
     3.4  {
     3.5    private def build(options: Options): (Build.Results, Time) =
     3.6    {
     3.7 -    val progress = new Console_Progress(true)
     3.8 +    val progress = new Console_Progress(verbose = true)
     3.9      val start_time = Time.now()
    3.10      val results = progress.interrupt_handler {
    3.11        Build.build_selection(
     4.1 --- a/src/Pure/Tools/ml_console.scala	Sat Oct 08 14:09:55 2016 +0200
     4.2 +++ b/src/Pure/Tools/ml_console.scala	Sat Oct 08 21:31:56 2016 +0200
     4.3 @@ -58,7 +58,7 @@
     4.4            !Build.build(options = options, build_heap = true, no_build = true,
     4.5              dirs = dirs, system_mode = system_mode, sessions = List(logic)).ok)
     4.6        {
     4.7 -        val progress = new Console_Progress
     4.8 +        val progress = new Console_Progress()
     4.9          progress.echo("Build started for Isabelle/" + logic + " ...")
    4.10          progress.interrupt_handler {
    4.11            val res =