tuned signature;
authorwenzelm
Wed, 22 May 2013 16:47:48 +0200
changeset 52115 3660205b96fa
parent 52114 fa497b99dccf
child 52116 abf9fcfa65cf
tuned signature;
src/Pure/Tools/build.scala
src/Pure/Tools/build_dialog.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)
             }
--- 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) }