# HG changeset patch # User wenzelm # Date 1475955116 -7200 # Node ID 68619fa37ca77d2953b46dcf6d32d2f63ad2a696 # Parent 45e065eea984b4504a0b26e0ec36d5a05667eab3 tuned; diff -r 45e065eea984 -r 68619fa37ca7 src/Pure/PIDE/batch_session.scala --- a/src/Pure/PIDE/batch_session.scala Sat Oct 08 14:09:55 2016 +0200 +++ b/src/Pure/PIDE/batch_session.scala Sat Oct 08 21:31:56 2016 +0200 @@ -23,7 +23,7 @@ val parent_session = session_info.parent getOrElse error("No parent session for " + quote(session)) - if (!Build.build(options, new Console_Progress(verbose), + if (!Build.build(options, new Console_Progress(verbose = verbose), verbose = verbose, build_heap = true, dirs = dirs, sessions = List(parent_session)).ok) new RuntimeException @@ -35,7 +35,7 @@ new Resources(content.loaded_theories, content.known_theories, content.syntax) } - val progress = new Console_Progress(verbose) + val progress = new Console_Progress(verbose = verbose) val prover_session = new Session(resources) val batch_session = new Batch_Session(prover_session) diff -r 45e065eea984 -r 68619fa37ca7 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sat Oct 08 14:09:55 2016 +0200 +++ b/src/Pure/Tools/build.scala Sat Oct 08 21:31:56 2016 +0200 @@ -750,7 +750,7 @@ val sessions = getopts(args) - val progress = new Console_Progress(verbose) + val progress = new Console_Progress(verbose = verbose) if (verbose) { progress.echo( diff -r 45e065eea984 -r 68619fa37ca7 src/Pure/Tools/ci_profile.scala --- a/src/Pure/Tools/ci_profile.scala Sat Oct 08 14:09:55 2016 +0200 +++ b/src/Pure/Tools/ci_profile.scala Sat Oct 08 21:31:56 2016 +0200 @@ -16,7 +16,7 @@ { private def build(options: Options): (Build.Results, Time) = { - val progress = new Console_Progress(true) + val progress = new Console_Progress(verbose = true) val start_time = Time.now() val results = progress.interrupt_handler { Build.build_selection( diff -r 45e065eea984 -r 68619fa37ca7 src/Pure/Tools/ml_console.scala --- a/src/Pure/Tools/ml_console.scala Sat Oct 08 14:09:55 2016 +0200 +++ b/src/Pure/Tools/ml_console.scala Sat Oct 08 21:31:56 2016 +0200 @@ -58,7 +58,7 @@ !Build.build(options = options, build_heap = true, no_build = true, dirs = dirs, system_mode = system_mode, sessions = List(logic)).ok) { - val progress = new Console_Progress + val progress = new Console_Progress() progress.echo("Build started for Isabelle/" + logic + " ...") progress.interrupt_handler { val res =