src/Pure/Tools/build.scala
changeset 62403 1d7aba20a332
parent 62402 bff56eae3ec5
child 62404 13a0f537e232
     1.1 --- a/src/Pure/Tools/build.scala	Wed Feb 24 23:36:45 2016 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Thu Feb 25 00:06:37 2016 +0100
     1.3 @@ -734,6 +734,14 @@
     1.4  
     1.5    /* build_results */
     1.6  
     1.7 +  class Build_Results private [Build](results: Map[String, Option[Process_Result]])
     1.8 +  {
     1.9 +    def sessions: Set[String] = results.keySet
    1.10 +    def cancelled(name: String): Boolean = results(name).isEmpty
    1.11 +    def process_result(name: String): Process_Result = results(name).getOrElse(Process_Result(1))
    1.12 +    val rc = (0 /: results.iterator.map({ case (_, Some(r)) => r.rc case (_, None) => 1 }))(_ max _)
    1.13 +  }
    1.14 +
    1.15    def build_results(
    1.16      options: Options,
    1.17      progress: Progress = Ignore_Progress,
    1.18 @@ -752,7 +760,7 @@
    1.19      system_mode: Boolean = false,
    1.20      verbose: Boolean = false,
    1.21      exclude_sessions: List[String] = Nil,
    1.22 -    sessions: List[String] = Nil): Map[String, Option[Process_Result]] =
    1.23 +    sessions: List[String] = Nil): Build_Results =
    1.24    {
    1.25      /* session tree and dependencies */
    1.26  
    1.27 @@ -980,10 +988,7 @@
    1.28        if (browser_chapters.nonEmpty) Present.make_global_index(browser_info)
    1.29      }
    1.30  
    1.31 -
    1.32 -    /* process results */
    1.33 -
    1.34 -    (for ((name, result) <- results.iterator) yield (name, result.process)).toMap
    1.35 +    new Build_Results((for ((name, result) <- results.iterator) yield (name, result.process)).toMap)
    1.36    }
    1.37  
    1.38  
    1.39 @@ -1014,16 +1019,16 @@
    1.40          dirs, select_dirs, exclude_session_groups, session_groups, max_jobs, list_files,
    1.41          check_keywords, no_build, system_mode, verbose, exclude_sessions, sessions)
    1.42  
    1.43 -    val rc = (0 /: results.iterator.flatMap(p => p._2.map(_.rc)))(_ max _)
    1.44 -    if (rc != 0 && (verbose || !no_build)) {
    1.45 +    if (results.rc != 0 && (verbose || !no_build)) {
    1.46        val unfinished =
    1.47          (for {
    1.48 -          (name, r) <- results.iterator
    1.49 -          if r.isEmpty || r.isDefined && !r.get.ok
    1.50 +          name <- results.sessions.iterator
    1.51 +          if !results.process_result(name).ok
    1.52           } yield name).toList.sorted
    1.53        progress.echo("Unfinished session(s): " + commas(unfinished))
    1.54      }
    1.55 -    rc
    1.56 +
    1.57 +    results.rc
    1.58    }
    1.59  
    1.60