--- 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 ...]
--- 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) {
--- 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)
--- 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
}
}
--- 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.
--- 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 + " ..."
--- 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)