# HG changeset patch
# User wenzelm
# Date 1590487122 -7200
# Node ID ce06d6456cc899aacf119d7d4eb10974f194afd9
# Parent  7a39036d5a19c436757b38be54e594309d9c7a2f
clarified signature --- fit within limit of 22 arguments;

diff -r 7a39036d5a19 -r ce06d6456cc8 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Tue May 26 11:25:33 2020 +0200
+++ b/src/Doc/System/Sessions.thy	Tue May 26 11:58:42 2020 +0200
@@ -291,7 +291,7 @@
   auxiliary files, and target heap images. Accordingly, it runs instances of
   the prover process with optional document preparation. Its command-line
   usage is:\<^footnote>\<open>Isabelle/Scala provides the same functionality via
-  \<^verbatim>\<open>isabelle.Build.build\<close>.\<close>
+  \<^scala_method>\<open>isabelle.Build.build\<close>.\<close>
   @{verbatim [display]
 \<open>Usage: isabelle build [OPTIONS] [SESSIONS ...]
 
diff -r 7a39036d5a19 -r ce06d6456cc8 src/Pure/Admin/build_doc.scala
--- a/src/Pure/Admin/build_doc.scala	Tue May 26 11:25:33 2020 +0200
+++ b/src/Pure/Admin/build_doc.scala	Tue May 26 11:58:42 2020 +0200
@@ -42,8 +42,8 @@
     progress.echo("Build started for documentation " + commas_quote(selected_docs))
 
     val res1 =
-      Build.build(options, progress, requirements = true, build_heap = true,
-        max_jobs = max_jobs, sessions = sessions)
+      Build.build(options, 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 +52,8 @@
               options.bool.update("browser_info", false).
                 string.update("document", "pdf").
                 string.update("document_output", output.implode),
-              progress, clean_build = true, max_jobs = max_jobs, sessions = sessions)
+              Sessions.Selection(sessions = sessions),
+              progress = progress, clean_build = true, max_jobs = max_jobs)
           if (res2.ok) {
             val doc_dir = Path.explode("~~/doc")
             for (doc <- selected_docs) {
diff -r 7a39036d5a19 -r ce06d6456cc8 src/Pure/Admin/ci_profile.scala
--- a/src/Pure/Admin/ci_profile.scala	Tue May 26 11:25:33 2020 +0200
+++ b/src/Pure/Admin/ci_profile.scala	Tue May 26 11:58:42 2020 +0200
@@ -20,15 +20,15 @@
     val start_time = Time.now()
     val results = progress.interrupt_handler {
       Build.build(
-        options = options + "system_heaps",
+        options + "system_heaps",
+        selection,
         progress = progress,
         clean_build = clean,
         verbose = true,
         numa_shuffling = numa,
         max_jobs = jobs,
         dirs = include,
-        select_dirs = select,
-        selection = selection)
+        select_dirs = select)
     }
     val end_time = Time.now()
     (results, end_time - start_time)
diff -r 7a39036d5a19 -r ce06d6456cc8 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue May 26 11:25:33 2020 +0200
+++ b/src/Pure/Tools/build.scala	Tue May 26 11:58:42 2020 +0200
@@ -469,6 +469,7 @@
 
   def build(
     options: Options,
+    selection: Sessions.Selection,
     progress: Progress = new Progress,
     check_unknown_files: Boolean = false,
     build_heap: Boolean = false,
@@ -484,15 +485,7 @@
     no_build: Boolean = false,
     soft_build: Boolean = false,
     verbose: Boolean = false,
-    export_files: Boolean = false,
-    requirements: Boolean = false,
-    all_sessions: Boolean = false,
-    base_sessions: List[String] = Nil,
-    exclude_session_groups: List[String] = Nil,
-    exclude_sessions: List[String] = Nil,
-    session_groups: List[String] = Nil,
-    sessions: List[String] = Nil,
-    selection: Sessions.Selection = Sessions.Selection.empty): Results =
+    export_files: Boolean = false): Results =
   {
     val build_options =
       options +
@@ -520,14 +513,10 @@
       SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString
     }
 
-    val selection1 =
-      Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
-        exclude_sessions, session_groups, sessions) ++ selection
-
     val deps =
     {
       val deps0 =
-        Sessions.deps(full_sessions.selection(selection1),
+        Sessions.deps(full_sessions.selection(selection),
           progress = progress, inlined_files = true, verbose = verbose,
           list_files = list_files, check_keywords = check_keywords).check_errors
 
@@ -577,7 +566,7 @@
     store.prepare_output_dir()
 
     if (clean_build) {
-      for (name <- full_sessions.imports_descendants(full_sessions.imports_selection(selection1))) {
+      for (name <- full_sessions.imports_descendants(full_sessions.imports_selection(selection))) {
         val (relevant, ok) = store.clean_output(name)
         if (relevant) {
           if (ok) progress.echo("Cleaned " + name)
@@ -765,7 +754,7 @@
           yield (name, (result.process, result.info))).toMap)
 
     if (export_files) {
-      for (name <- full_sessions.imports_selection(selection1).iterator if results(name).ok) {
+      for (name <- full_sessions.imports_selection(selection).iterator if results(name).ok) {
         val info = results.info(name)
         if (info.export_files.nonEmpty) {
           progress.echo("Exporting " + info.name + " ...")
@@ -903,6 +892,14 @@
     val results =
       progress.interrupt_handler {
         build(options,
+          Sessions.Selection(
+            requirements = requirements,
+            all_sessions = all_sessions,
+            base_sessions = base_sessions,
+            exclude_session_groups = exclude_session_groups,
+            exclude_sessions = exclude_sessions,
+            session_groups = session_groups,
+            sessions = sessions),
           progress = progress,
           check_unknown_files = Mercurial.is_repository(Path.explode("~~")),
           build_heap = build_heap,
@@ -917,14 +914,7 @@
           no_build = no_build,
           soft_build = soft_build,
           verbose = verbose,
-          export_files = export_files,
-          requirements = requirements,
-          all_sessions = all_sessions,
-          base_sessions = base_sessions,
-          exclude_session_groups = exclude_session_groups,
-          exclude_sessions = exclude_sessions,
-          session_groups = session_groups,
-          sessions = sessions)
+          export_files = export_files)
       }
     val end_date = Date.now()
     val elapsed_time = end_date.time - start_date.time
@@ -951,15 +941,15 @@
     fresh: Boolean = false,
     strict: Boolean = false): Int =
   {
+    val selection = Sessions.Selection.session(logic)
     val rc =
-      if (!fresh && build(options, build_heap = build_heap, no_build = true, dirs = dirs,
-          sessions = List(logic)).ok) 0
+      if (!fresh &&
+          build(options, selection, build_heap = build_heap, no_build = true, dirs = dirs).ok) 0
       else {
         progress.echo("Build started for Isabelle/" + logic + " ...")
-        Build.build(options, progress = progress, build_heap = build_heap, fresh_build = fresh,
-          dirs = dirs, sessions = List(logic)).rc
+        Build.build(options, 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
   }
 }
diff -r 7a39036d5a19 -r ce06d6456cc8 src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Tue May 26 11:25:33 2020 +0200
+++ b/src/Pure/Tools/server_commands.scala	Tue May 26 11:58:42 2020 +0200
@@ -57,13 +57,12 @@
       val base = base_info.check_base
 
       val results =
-        Build.build(options,
+        Build.build(options, Sessions.Selection.session(args.session),
           progress = progress,
           build_heap = true,
           dirs = dirs,
           infos = base_info.infos,
-          verbose = args.verbose,
-          sessions = List(args.session))
+          verbose = args.verbose)
 
       val sessions_order =
         base_info.sessions_structure.imports_topological_order.zipWithIndex.
diff -r 7a39036d5a19 -r ce06d6456cc8 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Tue May 26 11:25:33 2020 +0200
+++ b/src/Tools/VSCode/src/server.scala	Tue May 26 11:58:42 2020 +0200
@@ -269,8 +269,8 @@
         base_info.check_base
 
         def build(no_build: Boolean = false): Build.Results =
-          Build.build(options, build_heap = true, no_build = no_build, dirs = session_dirs,
-            infos = base_info.infos, sessions = List(base_info.session))
+          Build.build(options, 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) {
           val start_msg = "Build started for Isabelle/" + base_info.session + " ..."
diff -r 7a39036d5a19 -r ce06d6456cc8 src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Tue May 26 11:25:33 2020 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Tue May 26 11:58:42 2020 +0200
@@ -128,9 +128,9 @@
   def session_build(
     options: Options, progress: Progress = new Progress, no_build: Boolean = false): Int =
   {
-    Build.build(session_options(options), progress = progress, build_heap = true,
-      no_build = no_build, dirs = session_dirs(), infos = PIDE.resources.session_base_info.infos,
-      sessions = List(PIDE.resources.session_name)).rc
+    Build.build(session_options(options), 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
   }
 
   def session_start(options0: Options)