# HG changeset patch
# User wenzelm
# Date 1361361830 -3600
# Node ID 88c96e836ed6733e002b22358ded890393530341
# Parent  1973089f1dbacb5590a7e65fd39d1400511058de
prefer comparison of session timing, if this is known already;
some odd workarounds to prevent crashes due to TreeSet.- sometimes not deleting the element;

diff -r 1973089f1dba -r 88c96e836ed6 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Feb 20 11:40:30 2013 +0100
+++ b/src/Pure/Tools/build.scala	Wed Feb 20 13:03:50 2013 +0100
@@ -304,10 +304,18 @@
 
       object Ordering extends scala.math.Ordering[String]
       {
+        def compare_timing(name1: String, name2: String): Int =
+        {
+          val t1 = session_timing(name1)
+          val t2 = session_timing(name2)
+          if (t1 == 0.0 || t2 == 0.0) 0
+          else t1 compare t2
+        }
+
         def compare(name1: String, name2: String): Int =
-          outdegree(name2) compare outdegree(name1) match {
+          compare_timing(name2, name1) match {
             case 0 =>
-              session_timing(name2) compare session_timing(name1) match {
+              outdegree(name2) compare outdegree(name1) match {
                 case 0 =>
                   timeout(name2) compare timeout(name1) match {
                     case 0 => name1 compare name2
@@ -332,11 +340,17 @@
 
     def is_empty: Boolean = graph.is_empty
 
-    def - (name: String): Queue = new Queue(graph.del_node(name), order - name, command_timings)
+    def - (name: String): Queue =
+      new Queue(graph.del_node(name),
+        order - name,  // FIXME scala-2.10.0 TreeSet problem!?
+        command_timings)
 
     def dequeue(skip: String => Boolean): Option[(String, Session_Info)] =
     {
-      val it = order.iterator.dropWhile(name => skip(name) || !graph.is_minimal(name))
+      val it = order.iterator.dropWhile(name =>
+        skip(name)
+          || !graph.defined(name)  // FIXME scala-2.10.0 TreeSet problem!?
+          || !graph.is_minimal(name))
       if (it.hasNext) { val name = it.next; Some((name, graph.get_node(name))) }
       else None
     }