--- a/src/Pure/PIDE/batch_session.scala Wed Mar 16 21:14:59 2016 +0100
+++ b/src/Pure/PIDE/batch_session.scala Wed Mar 16 21:45:04 2016 +0100
@@ -23,9 +23,9 @@
val parent_session =
session_info.parent getOrElse error("No parent session for " + quote(session))
- if (Build.build(options, new Console_Progress(verbose),
+ if (!Build.build(options, new Console_Progress(verbose),
verbose = verbose, build_heap = true,
- dirs = dirs, sessions = List(parent_session)) != 0)
+ dirs = dirs, sessions = List(parent_session)).ok)
new RuntimeException
val deps = Build.dependencies(verbose = verbose, tree = session_tree)
--- a/src/Pure/Tools/build.scala Wed Mar 16 21:14:59 2016 +0100
+++ b/src/Pure/Tools/build.scala Wed Mar 16 21:45:04 2016 +0100
@@ -411,19 +411,20 @@
- /** build_results **/
+ /** build with results **/
- class Build_Results private [Build](results: Map[String, Option[Process_Result]])
+ class Results private [Build](results: Map[String, Option[Process_Result]])
{
def sessions: Set[String] = results.keySet
def cancelled(name: String): Boolean = results(name).isEmpty
def apply(name: String): Process_Result = results(name).getOrElse(Process_Result(1))
val rc = (0 /: results.iterator.map({ case (_, Some(r)) => r.rc case (_, None) => 1 }))(_ max _)
+ def ok: Boolean = rc == 0
override def toString: String = rc.toString
}
- def build_results(
+ def build(
options: Options,
progress: Progress = Ignore_Progress,
requirements: Boolean = false,
@@ -441,7 +442,7 @@
system_mode: Boolean = false,
verbose: Boolean = false,
exclude_sessions: List[String] = Nil,
- sessions: List[String] = Nil): Build_Results =
+ sessions: List[String] = Nil): Results =
{
/* session tree and dependencies */
@@ -642,20 +643,32 @@
/* build results */
- val results =
+ val results0 =
if (deps.is_empty) {
progress.echo(Output.warning_text("Nothing to build"))
Map.empty[String, Result]
}
else loop(queue, Map.empty, Map.empty)
+ val results =
+ new Results((for ((name, result) <- results0.iterator) yield (name, result.process)).toMap)
+
+ if (results.rc != 0 && (verbose || !no_build)) {
+ val unfinished =
+ (for {
+ name <- results.sessions.iterator
+ if !results(name).ok
+ } yield name).toList.sorted
+ progress.echo("Unfinished session(s): " + commas(unfinished))
+ }
+
/* global browser info */
if (!no_build) {
val browser_chapters =
(for {
- (name, result) <- results.iterator
+ (name, result) <- results0.iterator
if result.ok && !Sessions.is_pure(name)
info = full_tree(name)
if info.options.bool("browser_info")
@@ -668,48 +681,7 @@
if (browser_chapters.nonEmpty) Present.make_global_index(store.browser_info)
}
- new Build_Results((for ((name, result) <- results.iterator) yield (name, result.process)).toMap)
- }
-
-
-
- /** build **/
-
- def build(
- options: Options,
- progress: Progress = Ignore_Progress,
- requirements: Boolean = false,
- all_sessions: Boolean = false,
- build_heap: Boolean = false,
- clean_build: Boolean = false,
- dirs: List[Path] = Nil,
- select_dirs: List[Path] = Nil,
- exclude_session_groups: List[String] = Nil,
- session_groups: List[String] = Nil,
- max_jobs: Int = 1,
- list_files: Boolean = false,
- check_keywords: Set[String] = Set.empty,
- no_build: Boolean = false,
- system_mode: Boolean = false,
- verbose: Boolean = false,
- exclude_sessions: List[String] = Nil,
- sessions: List[String] = Nil): Int =
- {
- val results =
- build_results(options, progress, requirements, all_sessions, build_heap, clean_build,
- dirs, select_dirs, exclude_session_groups, session_groups, max_jobs, list_files,
- check_keywords, no_build, system_mode, verbose, exclude_sessions, sessions)
-
- if (results.rc != 0 && (verbose || !no_build)) {
- val unfinished =
- (for {
- name <- results.sessions.iterator
- if !results(name).ok
- } yield name).toList.sorted
- progress.echo("Unfinished session(s): " + commas(unfinished))
- }
-
- results.rc
+ results
}
@@ -805,7 +777,7 @@
val start_time = Time.now()
val results =
progress.interrupt_handler {
- build_results(options, progress, requirements, all_sessions, build_heap, clean_build,
+ build(options, progress, requirements, all_sessions, build_heap, clean_build,
dirs, select_dirs, exclude_session_groups, session_groups, max_jobs, list_files,
check_keywords, no_build, system_mode, verbose, exclude_sessions, sessions)
}
--- a/src/Pure/Tools/build_doc.scala Wed Mar 16 21:14:59 2016 +0100
+++ b/src/Pure/Tools/build_doc.scala Wed Mar 16 21:45:04 2016 +0100
@@ -40,30 +40,30 @@
progress.echo("Build started for documentation " + commas_quote(selected_docs))
- val rc1 =
+ val res1 =
Build.build(options, progress, requirements = true, build_heap = true,
max_jobs = max_jobs, system_mode = system_mode, sessions = sessions)
- if (rc1 == 0) {
+ if (res1.ok) {
Isabelle_System.with_tmp_dir("document_output")(output =>
{
- val rc2 =
+ val res2 =
Build.build(
options.bool.update("browser_info", false).
string.update("document", "pdf").
string.update("document_output", File.standard_path(output)),
progress, clean_build = true, max_jobs = max_jobs, system_mode = system_mode,
sessions = sessions)
- if (rc2 == 0) {
+ if (res2.ok) {
val doc_dir = Path.explode("$ISABELLE_HOME/doc").file
for (doc <- selected_docs) {
val name = doc + ".pdf"
File.copy(new JFile(output, name), new JFile(doc_dir, name))
}
}
- rc2
+ res2.rc
})
}
- else rc1
+ else res1.rc
}
--- a/src/Pure/Tools/ml_console.scala Wed Mar 16 21:14:59 2016 +0100
+++ b/src/Pure/Tools/ml_console.scala Wed Mar 16 21:45:04 2016 +0100
@@ -54,16 +54,16 @@
// build
if (!no_build && logic != "RAW_ML_SYSTEM" &&
- Build.build(options = options, build_heap = true, no_build = true,
- dirs = dirs, system_mode = system_mode, sessions = List(logic)) != 0)
+ !Build.build(options = 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 rc =
+ val res =
Build.build(options = options, progress = progress, build_heap = true,
dirs = dirs, system_mode = system_mode, sessions = List(logic))
- if (rc != 0) sys.exit(rc)
+ if (!res.ok) sys.exit(res.rc)
}
}
--- a/src/Tools/jEdit/src/isabelle_logic.scala Wed Mar 16 21:14:59 2016 +0100
+++ b/src/Tools/jEdit/src/isabelle_logic.scala Wed Mar 16 21:45:04 2016 +0100
@@ -66,7 +66,7 @@
Build.build(options = PIDE.options.value, progress = progress,
build_heap = true, no_build = no_build, system_mode = mode == "" || mode == "system",
- dirs = session_dirs(), sessions = List(session_name()))
+ dirs = session_dirs(), sessions = List(session_name())).rc
}
def session_start()