# HG changeset patch # User wenzelm # Date 1456353405 -3600 # Node ID bff56eae3ec53df204fd00ef32caa4606cf62f70 # Parent 15a2533f1f0ad5ef63532d1996028bb4f0407353 more informative Build.build_results; tuned signature; diff -r 15a2533f1f0a -r bff56eae3ec5 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Wed Feb 24 22:40:19 2016 +0100 +++ b/src/Pure/System/isabelle_system.scala Wed Feb 24 23:36:45 2016 +0100 @@ -337,7 +337,7 @@ catch { case Exn.Interrupt() => proc.terminate; Exn.Interrupt.return_code } if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt() - Process_Result(stdout.join, stderr.join, rc, None) + Process_Result(rc, out_lines = stdout.join, err_lines = stderr.join) } } diff -r 15a2533f1f0a -r bff56eae3ec5 src/Pure/System/process_result.scala --- a/src/Pure/System/process_result.scala Wed Feb 24 22:40:19 2016 +0100 +++ b/src/Pure/System/process_result.scala Wed Feb 24 23:36:45 2016 +0100 @@ -7,7 +7,10 @@ package isabelle final case class Process_Result( - out_lines: List[String], err_lines: List[String], rc: Int, timeout: Option[Time]) + rc: Int, + out_lines: List[String] = Nil, + err_lines: List[String] = Nil, + timeout: Option[Time] = None) { def out: String = cat_lines(out_lines) def err: String = cat_lines(err_lines) @@ -25,10 +28,12 @@ else if (interrupted) throw Exn.Interrupt() else Library.error(err) + def clear: Process_Result = copy(out_lines = Nil, err_lines = Nil) + def print: Process_Result = { Output.warning(Library.trim_line(err)) Output.writeln(Library.trim_line(out)) - copy(out_lines = Nil, err_lines = Nil) + clear } } diff -r 15a2533f1f0a -r bff56eae3ec5 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Feb 24 22:40:19 2016 +0100 +++ b/src/Pure/Tools/build.scala Wed Feb 24 23:36:45 2016 +0100 @@ -752,7 +752,7 @@ 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 */ @@ -835,7 +835,14 @@ } // 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() { @@ -887,7 +894,7 @@ 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 @@ -895,7 +902,7 @@ 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) @@ -918,12 +925,14 @@ 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, @@ -932,7 +941,7 @@ } 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) } @@ -959,7 +968,7 @@ 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). @@ -972,9 +981,9 @@ } - /* results */ + /* process results */ - results.map({ case (name, result) => (name, result.rc) }) + (for ((name, result) <- results.iterator) yield (name, result.process)).toMap } @@ -1005,10 +1014,13 @@ 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