tuned;
authorwenzelm
Tue, 13 Mar 2018 18:28:12 +0100
changeset 67846 bdf6933f7ac9
parent 67845 46fa8c2c142a
child 67847 c61acb4855b6
tuned;
src/Pure/ML/ml_console.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
src/Tools/VSCode/src/server.scala
src/Tools/jEdit/src/jedit_sessions.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)
         }
--- 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,
--- 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,
--- 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)
--- 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
   }