--- 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
}