# HG changeset patch
# User wenzelm
# Date 1520962092 -3600
# Node ID bdf6933f7ac955417d1b84ba2297e2a21deef97f
# Parent  46fa8c2c142a893d24e73b10f75caed6715a062e
tuned;

diff -r 46fa8c2c142a -r bdf6933f7ac9 src/Pure/ML/ml_console.scala
--- a/src/Pure/ML/ml_console.scala	Tue Mar 13 17:15:01 2018 +0100
+++ b/src/Pure/ML/ml_console.scala	Tue Mar 13 18:28:12 2018 +0100
@@ -52,14 +52,14 @@
 
       // build
       if (!no_build && !raw_ml_system &&
-          !Build.build(options = options, build_heap = true, no_build = true,
+          !Build.build(options, build_heap = true, no_build = true,
             dirs = dirs, system_mode = system_mode, sessions = List(logic)).ok)
       {
         val progress = new Console_Progress()
         progress.echo("Build started for Isabelle/" + logic + " ...")
         progress.interrupt_handler {
           val res =
-            Build.build(options = options, progress = progress, build_heap = true,
+            Build.build(options, progress = progress, build_heap = true,
               dirs = dirs, system_mode = system_mode, sessions = List(logic))
           if (!res.ok) sys.exit(res.rc)
         }
diff -r 46fa8c2c142a -r bdf6933f7ac9 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Mar 13 17:15:01 2018 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Mar 13 18:28:12 2018 +0100
@@ -367,7 +367,8 @@
     def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors))
   }
 
-  def base_info(options: Options, session: String,
+  def base_info(options: Options,
+    session: String,
     dirs: List[Path] = Nil,
     ancestor_session: Option[String] = None,
     all_known: Boolean = false,
diff -r 46fa8c2c142a -r bdf6933f7ac9 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Mar 13 17:15:01 2018 +0100
+++ b/src/Pure/Tools/build.scala	Tue Mar 13 18:28:12 2018 +0100
@@ -770,7 +770,8 @@
 
     val results =
       progress.interrupt_handler {
-        build(options, progress,
+        build(options,
+          progress = progress,
           check_unknown_files = Mercurial.is_repository(Path.explode("~~")),
           build_heap = build_heap,
           clean_build = clean_build,
diff -r 46fa8c2c142a -r bdf6933f7ac9 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Tue Mar 13 17:15:01 2018 +0100
+++ b/src/Tools/VSCode/src/server.scala	Tue Mar 13 18:28:12 2018 +0100
@@ -252,8 +252,8 @@
 
     val try_session =
       try {
-        if (!Build.build(options = options, build_heap = true, no_build = true,
-              system_mode = system_mode, dirs = session_dirs, sessions = List(session_name)).ok)
+        if (!Build.build(options, build_heap = true, no_build = true,
+            system_mode = system_mode, dirs = session_dirs, sessions = List(session_name)).ok)
         {
           val start_msg = "Build started for Isabelle/" + session_name + " ..."
           val fail_msg = "Session build failed -- prover process remains inactive!"
@@ -261,7 +261,7 @@
           val progress = channel.make_progress(verbose = true)
           progress.echo(start_msg); channel.writeln(start_msg)
 
-          if (!Build.build(options = options, progress = progress, build_heap = true,
+          if (!Build.build(options, progress = progress, build_heap = true,
               system_mode = system_mode, dirs = session_dirs, sessions = List(session_name)).ok)
           {
             progress.echo(fail_msg); error(fail_msg)
diff -r 46fa8c2c142a -r bdf6933f7ac9 src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Tue Mar 13 17:15:01 2018 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Tue Mar 13 18:28:12 2018 +0100
@@ -124,8 +124,8 @@
   {
     val mode = session_build_mode()
 
-    Build.build(options = session_options(options), progress = progress,
-      build_heap = true, no_build = no_build, system_mode = mode == "" || mode == "system",
+    Build.build(session_options(options), progress = progress, build_heap = true,
+      no_build = no_build, system_mode = mode == "" || mode == "system",
       dirs = session_dirs(), infos = PIDE.resources.session_base_info.infos,
       sessions = List(PIDE.resources.session_name)).rc
   }