# HG changeset patch # User wenzelm # Date 1369234068 -7200 # Node ID 3660205b96fa9d21f14982ed84e0c08d23c5e516 # Parent fa497b99dccf1f40806f4f13a343788f662f38c4 tuned signature; diff -r fa497b99dccf -r 3660205b96fa src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed May 22 16:42:13 2013 +0200 +++ b/src/Pure/Tools/build.scala Wed May 22 16:47:48 2013 +0200 @@ -651,8 +651,8 @@ /* build_results */ def build_results( - progress: Progress, options: Options, + progress: Progress = Ignore_Progress, requirements: Boolean = false, all_sessions: Boolean = false, build_heap: Boolean = false, @@ -898,8 +898,8 @@ /* build */ def build( - progress: Progress, options: Options, + progress: Progress = Ignore_Progress, requirements: Boolean = false, all_sessions: Boolean = false, build_heap: Boolean = false, @@ -914,7 +914,7 @@ sessions: List[String] = Nil): Int = { val results = - build_results(progress, options, requirements, all_sessions, + build_results(options, progress, requirements, all_sessions, build_heap, clean_build, more_dirs, session_groups, max_jobs, list_files, no_build, system_mode, verbose, sessions) @@ -951,7 +951,7 @@ include_dirs.map(d => (false, Path.explode(d))) val progress = new Console_Progress(verbose) progress.interrupt_handler { - build(progress, options, requirements, all_sessions, + build(options, progress, requirements, all_sessions, build_heap, clean_build, more_dirs, session_groups, max_jobs, list_files, no_build, system_mode, verbose, sessions) } diff -r fa497b99dccf -r 3660205b96fa src/Pure/Tools/build_dialog.scala --- a/src/Pure/Tools/build_dialog.scala Wed May 22 16:42:13 2013 +0200 +++ b/src/Pure/Tools/build_dialog.scala Wed May 22 16:47:48 2013 +0200 @@ -33,7 +33,7 @@ Isabelle_System.default_logic(logic, if (logic_option != "") options.string(logic_option) else "") - if (Build.build(Build.Ignore_Progress, options, build_heap = true, no_build = true, + if (Build.build(options = options, build_heap = true, no_build = true, more_dirs = more_dirs, sessions = List(session)) == 0) sys.exit(0) else Swing_Thread.later { @@ -167,7 +167,8 @@ val (out, rc) = try { ("", - Build.build(progress, options, build_heap = true, more_dirs = more_dirs, + Build.build(options = options, progress = progress, + build_heap = true, more_dirs = more_dirs, system_mode = system_mode, sessions = List(session))) } catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) }