src/Pure/System/build.scala
changeset 48678 ff27af15530c
parent 48676 3ef82491cdd6
child 48680 463daacae6c2
equal deleted inserted replaced
48677:bd4d132e32cf 48678:ff27af15530c
   244   object Queue
   244   object Queue
   245   {
   245   {
   246     def apply(tree: Session_Tree): Queue =
   246     def apply(tree: Session_Tree): Queue =
   247     {
   247     {
   248       val graph = tree.graph
   248       val graph = tree.graph
   249       new Queue(graph, SortedSet(graph.keys.toList: _*)(graph.ordering))
   249 
       
   250       def outdegree(name: String): Int = graph.imm_succs(name).size
       
   251       def timeout(name: String): Double = tree(name).options.real("timeout")
       
   252 
       
   253       object Ordering extends scala.math.Ordering[String]
       
   254       {
       
   255         def compare(name1: String, name2: String): Int =
       
   256           outdegree(name2) compare outdegree(name1) match {
       
   257             case 0 =>
       
   258               timeout(name2) compare timeout(name1) match {
       
   259                 case 0 => name1 compare name2
       
   260                 case ord => ord
       
   261               }
       
   262             case ord => ord
       
   263           }
       
   264       }
       
   265 
       
   266       new Queue(graph, SortedSet(graph.keys.toList: _*)(Ordering))
   250     }
   267     }
   251   }
   268   }
   252 
   269 
   253   final class Queue private(graph: Graph[String, Option[Session_Info]], order: SortedSet[String])
   270   final class Queue private(graph: Graph[String, Option[Session_Info]], order: SortedSet[String])
   254   {
   271   {
   591                 }
   608                 }
   592                 val all_current = current && parent_result.current
   609                 val all_current = current && parent_result.current
   593 
   610 
   594                 if (all_current)
   611                 if (all_current)
   595                   loop(pending - name, running, results + (name -> Result(true, heap, 0)))
   612                   loop(pending - name, running, results + (name -> Result(true, heap, 0)))
   596                 else if (no_build)
   613                 else if (no_build) {
       
   614                   if (verbose) echo("Skipping " + name + " ...")
   597                   loop(pending - name, running, results + (name -> Result(false, heap, 1)))
   615                   loop(pending - name, running, results + (name -> Result(false, heap, 1)))
       
   616                 }
   598                 else if (parent_result.rc == 0) {
   617                 else if (parent_result.rc == 0) {
   599                   echo((if (do_output) "Building " else "Running ") + name + " ...")
   618                   echo((if (do_output) "Building " else "Running ") + name + " ...")
   600                   val job = new Job(name, info, output, do_output, verbose, browser_info)
   619                   val job = new Job(name, info, output, do_output, verbose, browser_info)
   601                   loop(pending, running + (name -> (parent_result.heap, job)), results)
   620                   loop(pending, running + (name -> (parent_result.heap, job)), results)
   602                 }
   621                 }