tuned signature;
authorwenzelm
Fri Mar 17 11:35:03 2017 +0100 (2017-03-17)
changeset 6528986d93effc3df
parent 65288 6934d0878634
child 65290 6c1d7d5c2165
tuned signature;
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Tools/build.scala	Fri Mar 17 11:27:58 2017 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Fri Mar 17 11:35:03 2017 +0100
     1.3 @@ -21,16 +21,46 @@
     1.4  {
     1.5    /** auxiliary **/
     1.6  
     1.7 -  /* queue */
     1.8 +  /* queue with scheduling information */
     1.9  
    1.10    private object Queue
    1.11    {
    1.12 -    def apply(tree: Sessions.Tree, load_timings: String => (List[Properties.T], Double)): Queue =
    1.13 +    def load_timings(store: Sessions.Store, name: String): (List[Properties.T], Double) =
    1.14 +    {
    1.15 +      val (path, text) =
    1.16 +        store.find_log_gz(name) match {
    1.17 +          case Some(path) => (path, File.read_gzip(path))
    1.18 +          case None =>
    1.19 +            store.find_log(name) match {
    1.20 +              case Some(path) => (path, File.read(path))
    1.21 +              case None => (Path.current, "")
    1.22 +            }
    1.23 +        }
    1.24 +
    1.25 +      def ignore_error(msg: String): (List[Properties.T], Double) =
    1.26 +      {
    1.27 +        Output.warning("Ignoring bad log file: " + path + (if (msg == "") "" else "\n" + msg))
    1.28 +        (Nil, 0.0)
    1.29 +      }
    1.30 +
    1.31 +      try {
    1.32 +        val info = Build_Log.Log_File(name, text).parse_session_info(name, command_timings = true)
    1.33 +        val session_timing = Markup.Elapsed.unapply(info.session_timing) getOrElse 0.0
    1.34 +        (info.command_timings, session_timing)
    1.35 +      }
    1.36 +      catch {
    1.37 +        case ERROR(msg) => ignore_error(msg)
    1.38 +        case exn: java.lang.Error => ignore_error(Exn.message(exn))
    1.39 +        case _: XML.Error => ignore_error("")
    1.40 +      }
    1.41 +    }
    1.42 +
    1.43 +    def apply(tree: Sessions.Tree, store: Sessions.Store): Queue =
    1.44      {
    1.45        val graph = tree.graph
    1.46        val sessions = graph.keys
    1.47  
    1.48 -      val timings = Par_List.map((name: String) => (name, load_timings(name)), sessions)
    1.49 +      val timings = Par_List.map((name: String) => (name, load_timings(store, name)), sessions)
    1.50        val command_timings =
    1.51          Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
    1.52        val session_timing =
    1.53 @@ -329,46 +359,12 @@
    1.54      def session_sources_stamp(name: String): String =
    1.55        sources_stamp(selected_tree(name).meta_digest :: deps.sources(name))
    1.56  
    1.57 -    val store = Sessions.store(system_mode)
    1.58 -
    1.59 -
    1.60 -    /* queue with scheduling information */
    1.61 -
    1.62 -    def load_timings(name: String): (List[Properties.T], Double) =
    1.63 -    {
    1.64 -      val (path, text) =
    1.65 -        store.find_log_gz(name) match {
    1.66 -          case Some(path) => (path, File.read_gzip(path))
    1.67 -          case None =>
    1.68 -            store.find_log(name) match {
    1.69 -              case Some(path) => (path, File.read(path))
    1.70 -              case None => (Path.current, "")
    1.71 -            }
    1.72 -        }
    1.73 -
    1.74 -      def ignore_error(msg: String): (List[Properties.T], Double) =
    1.75 -      {
    1.76 -        Output.warning("Ignoring bad log file: " + path + (if (msg == "") "" else "\n" + msg))
    1.77 -        (Nil, 0.0)
    1.78 -      }
    1.79 -
    1.80 -      try {
    1.81 -        val info = Build_Log.Log_File(name, text).parse_session_info(name, command_timings = true)
    1.82 -        val session_timing = Markup.Elapsed.unapply(info.session_timing) getOrElse 0.0
    1.83 -        (info.command_timings, session_timing)
    1.84 -      }
    1.85 -      catch {
    1.86 -        case ERROR(msg) => ignore_error(msg)
    1.87 -        case exn: java.lang.Error => ignore_error(Exn.message(exn))
    1.88 -        case _: XML.Error => ignore_error("")
    1.89 -      }
    1.90 -    }
    1.91 -
    1.92 -    val queue = Queue(selected_tree, load_timings)
    1.93 -
    1.94  
    1.95      /* main build process */
    1.96  
    1.97 +    val store = Sessions.store(system_mode)
    1.98 +    val queue = Queue(selected_tree, store)
    1.99 +
   1.100      store.prepare_output()
   1.101  
   1.102      // optional cleanup