clarified signature;
authorwenzelm
Sat, 27 Jun 2020 11:25:30 +0200
changeset 71981 0be06f99b210
parent 71980 6441b4591eb8
child 71982 cea6087e8a70
clarified signature;
src/Pure/Admin/build_doc.scala
src/Pure/Admin/ci_profile.scala
src/Pure/Tools/build.scala
src/Pure/Tools/server_commands.scala
src/Tools/VSCode/src/server.scala
src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Pure/Admin/build_doc.scala	Fri Jun 26 17:34:34 2020 +0200
+++ b/src/Pure/Admin/build_doc.scala	Sat Jun 27 11:25:30 2020 +0200
@@ -42,7 +42,8 @@
     progress.echo("Build started for documentation " + commas_quote(selected_docs))
 
     val res1 =
-      Build.build(options, Sessions.Selection(requirements = true, sessions = sessions),
+      Build.build(options,
+        selection = Sessions.Selection(requirements = true, sessions = sessions),
         progress = progress, build_heap = true, max_jobs = max_jobs)
     if (res1.ok) {
       Isabelle_System.with_tmp_dir("document_output")(output =>
@@ -52,7 +53,7 @@
               options.bool.update("browser_info", false).
                 string.update("document", "pdf").
                 string.update("document_output", output.implode),
-              Sessions.Selection(sessions = sessions),
+              selection = Sessions.Selection(sessions = sessions),
               progress = progress, clean_build = true, max_jobs = max_jobs)
           if (res2.ok) {
             val doc_dir = Path.explode("~~/doc")
--- a/src/Pure/Admin/ci_profile.scala	Fri Jun 26 17:34:34 2020 +0200
+++ b/src/Pure/Admin/ci_profile.scala	Sat Jun 27 11:25:30 2020 +0200
@@ -21,7 +21,7 @@
     val results = progress.interrupt_handler {
       Build.build(
         options + "system_heaps",
-        selection,
+        selection = selection,
         progress = progress,
         clean_build = clean,
         verbose = true,
--- a/src/Pure/Tools/build.scala	Fri Jun 26 17:34:34 2020 +0200
+++ b/src/Pure/Tools/build.scala	Sat Jun 27 11:25:30 2020 +0200
@@ -462,7 +462,7 @@
 
   def build(
     options: Options,
-    selection: Sessions.Selection,
+    selection: Sessions.Selection = Sessions.Selection.empty,
     progress: Progress = new Progress,
     check_unknown_files: Boolean = false,
     build_heap: Boolean = false,
@@ -885,7 +885,7 @@
     val results =
       progress.interrupt_handler {
         build(options,
-          Sessions.Selection(
+          selection = Sessions.Selection(
             requirements = requirements,
             all_sessions = all_sessions,
             base_sessions = base_sessions,
@@ -936,12 +936,12 @@
   {
     val selection = Sessions.Selection.session(logic)
     val rc =
-      if (!fresh &&
-          build(options, selection, build_heap = build_heap, no_build = true, dirs = dirs).ok) 0
+      if (!fresh && build(options, selection = selection,
+            build_heap = build_heap, no_build = true, dirs = dirs).ok) 0
       else {
         progress.echo("Build started for Isabelle/" + logic + " ...")
-        Build.build(options, selection, progress = progress, build_heap = build_heap,
-          fresh_build = fresh, dirs = dirs).rc
+        Build.build(options, selection = selection, progress = progress,
+          build_heap = build_heap, fresh_build = fresh, dirs = dirs).rc
       }
     if (strict && rc != 0) error("Failed to build Isabelle/" + logic) else rc
   }
--- a/src/Pure/Tools/server_commands.scala	Fri Jun 26 17:34:34 2020 +0200
+++ b/src/Pure/Tools/server_commands.scala	Sat Jun 27 11:25:30 2020 +0200
@@ -57,7 +57,8 @@
       val base = base_info.check_base
 
       val results =
-        Build.build(options, Sessions.Selection.session(args.session),
+        Build.build(options,
+          selection = Sessions.Selection.session(args.session),
           progress = progress,
           build_heap = true,
           dirs = dirs,
--- a/src/Tools/VSCode/src/server.scala	Fri Jun 26 17:34:34 2020 +0200
+++ b/src/Tools/VSCode/src/server.scala	Sat Jun 27 11:25:30 2020 +0200
@@ -269,7 +269,8 @@
         base_info.check_base
 
         def build(no_build: Boolean = false): Build.Results =
-          Build.build(options, Sessions.Selection.session(base_info.session),
+          Build.build(options,
+            selection = Sessions.Selection.session(base_info.session),
             build_heap = true, no_build = no_build, dirs = session_dirs, infos = base_info.infos)
 
         if (!build(no_build = true).ok) {
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Fri Jun 26 17:34:34 2020 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Sat Jun 27 11:25:30 2020 +0200
@@ -128,7 +128,8 @@
   def session_build(
     options: Options, progress: Progress = new Progress, no_build: Boolean = false): Int =
   {
-    Build.build(session_options(options), Sessions.Selection.session(PIDE.resources.session_name),
+    Build.build(session_options(options),
+      selection = Sessions.Selection.session(PIDE.resources.session_name),
       progress = progress, build_heap = true, no_build = no_build, dirs = session_dirs(),
       infos = PIDE.resources.session_base_info.infos).rc
   }