src/Pure/Tools/build.scala

     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): Map[String, Int] =
+    sessions: List[String] = Nil): Map[String, Option[Process_Result]] =
   {
     /* session tree and dependencies */
 
     val full_tree = find_sessions(options.int("completion_limit") = 0, dirs, select_dirs)
     val (selected, selected_tree) =

         if (!files.forall(p => p.file.delete)) progress.echo(name + " FAILED to delete")
       }
     }
 
     // scheduler loop
-    case class Result(current: Boolean, heap: String, rc: Int)
+    case class Result(current: Boolean, heap: String, process: Option[Process_Result])
+    {
+      def ok: Boolean =
+        process match {
+          case None => false
+          case Some(res) => res.rc == 0
+        }
+    }
 
     def sleep()
     {
       try { Thread.sleep(500) }
       catch { case Exn.Interrupt() => Exn.Interrupt.impose() }

                 }
 
                 no_heap
               }
             loop(pending - name, running - name,
-              results + (name -> Result(false, heap, process_result.rc)))
+              results + (name -> Result(false, heap, Some(process_result.clear))))
             //}}}
           case None if running.size < (max_jobs max 1) =>
             //{{{ check/start next job
             pending.dequeue(running.isDefinedAt(_)) match {
               case Some((name, info)) =>
                 val parent_result =
                   info.parent match {
-                    case None => Result(true, no_heap, 0)
+                    case None => Result(true, no_heap, Some(Process_Result(0)))
                     case Some(parent) => results(parent)
                   }
                 val output = output_dir + Path.basic(name)
                 val do_output = build_heap || queue.is_inner(name)
 

                   }
                 }
                 val all_current = current && parent_result.current
 
                 if (all_current)
-                  loop(pending - name, running, results + (name -> Result(true, heap, 0)))
+                  loop(pending - name, running,
+                    results + (name -> Result(true, heap, Some(Process_Result(0)))))
                 else if (no_build) {
                   if (verbose) progress.echo("Skipping " + name + " ...")
-                  loop(pending - name, running, results + (name -> Result(false, heap, 1)))
+                  loop(pending - name, running,
+                    results + (name -> Result(false, heap, Some(Process_Result(1)))))
                 }
-                else if (parent_result.rc == 0 && !progress.stopped) {
+                else if (parent_result.ok && !progress.stopped) {
                   progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
                   val job =
                     new Job(progress, name, info, output, do_output, verbose, browser_info,
                       deps(name).session_graph, queue.command_timings(name))
                   loop(pending, running + (name -> (parent_result.heap, job)), results)
                 }
                 else {
                   progress.echo(name + " CANCELLED")
-                  loop(pending - name, running, results + (name -> Result(false, heap, 1)))
+                  loop(pending - name, running, results + (name -> Result(false, heap, None)))
                 }
               case None => sleep(); loop(pending, running, results)
             }
             ///}}}
           case None => sleep(); loop(pending, running, results)

 
     if (!no_build) {
       val browser_chapters =
         (for {
           (name, result) <- results.iterator
-          if result.rc == 0 && !is_pure(name)
+          if result.ok && !is_pure(name)
           info = full_tree(name)
           if info.options.bool("browser_info")
         } yield (info.chapter, (name, info.description))).toList.groupBy(_._1).
             map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
 

 
       if (browser_chapters.nonEmpty) Present.make_global_index(browser_info)
     }
 
 
-    /* results */
-
-    results.map({ case (name, result) => (name, result.rc) })
+    /* process results */
+
+    (for ((name, result) <- results.iterator) yield (name, result.process)).toMap
   }
 
 
   /* build */
 

     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)
 
-    val rc = (0 /: results)({ case (rc1, (_, rc2)) => rc1 max rc2 })
+    val rc = (0 /: results.iterator.flatMap(p => p._2.map(_.rc)))(_ max _)
     if (rc != 0 && (verbose || !no_build)) {
       val unfinished =
-        (for ((name, r) <- results.iterator if r != 0) yield name).toList.sorted
+        (for {
+          (name, r) <- results.iterator
+          if r.isEmpty || r.isDefined && !r.get.ok
+         } yield name).toList.sorted
       progress.echo("Unfinished session(s): " + commas(unfinished))
     }
     rc
   }