# HG changeset patch
# User wenzelm
# Date 1456355197 -3600
# Node ID 1d7aba20a332345156a951f7d91f1c7681308ee3
# Parent  bff56eae3ec53df204fd00ef32caa4606cf62f70
explicit class Build_Results;
cancelled sessions have rc = 1 (again);

diff -r bff56eae3ec5 -r 1d7aba20a332 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Feb 24 23:36:45 2016 +0100
+++ b/src/Pure/Tools/build.scala	Thu Feb 25 00:06:37 2016 +0100
@@ -734,6 +734,14 @@
 
   /* build_results */
 
+  class Build_Results private [Build](results: Map[String, Option[Process_Result]])
+  {
+    def sessions: Set[String] = results.keySet
+    def cancelled(name: String): Boolean = results(name).isEmpty
+    def process_result(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 build_results(
     options: Options,
     progress: Progress = Ignore_Progress,
@@ -752,7 +760,7 @@
     system_mode: Boolean = false,
     verbose: Boolean = false,
     exclude_sessions: List[String] = Nil,
-    sessions: List[String] = Nil): Map[String, Option[Process_Result]] =
+    sessions: List[String] = Nil): Build_Results =
   {
     /* session tree and dependencies */
 
@@ -980,10 +988,7 @@
       if (browser_chapters.nonEmpty) Present.make_global_index(browser_info)
     }
 
-
-    /* process results */
-
-    (for ((name, result) <- results.iterator) yield (name, result.process)).toMap
+    new Build_Results((for ((name, result) <- results.iterator) yield (name, result.process)).toMap)
   }
 
 
@@ -1014,16 +1019,16 @@
         dirs, select_dirs, exclude_session_groups, session_groups, max_jobs, list_files,
         check_keywords, no_build, system_mode, verbose, exclude_sessions, sessions)
 
-    val rc = (0 /: results.iterator.flatMap(p => p._2.map(_.rc)))(_ max _)
-    if (rc != 0 && (verbose || !no_build)) {
+    if (results.rc != 0 && (verbose || !no_build)) {
       val unfinished =
         (for {
-          (name, r) <- results.iterator
-          if r.isEmpty || r.isDefined && !r.get.ok
+          name <- results.sessions.iterator
+          if !results.process_result(name).ok
          } yield name).toList.sorted
       progress.echo("Unfinished session(s): " + commas(unfinished))
     }
-    rc
+
+    results.rc
   }