# HG changeset patch
# User wenzelm
# Date 1614877456 -3600
# Node ID a78b5ffc0f463e14e98c5b0d54e648ff345e40bb
# Parent  6bf6160a2c5483545c9ce011b0d9998954adddbb
more robust ordering (see also 88c96e836ed6);

diff -r 6bf6160a2c54 -r a78b5ffc0f46 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Mar 04 16:23:34 2021 +0100
+++ b/src/Pure/Tools/build.scala	Thu Mar 04 18:04:16 2021 +0100
@@ -99,16 +99,8 @@
 
       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 =
-          compare_timing(name2, name1) match {
+          session_timing(name2) compare session_timing(name1) match {
             case 0 =>
               sessions_structure(name2).timeout compare sessions_structure(name1).timeout match {
                 case 0 => name1 compare name2
@@ -132,16 +124,11 @@
     def is_empty: Boolean = graph.is_empty
 
     def - (name: String): Queue =
-      new Queue(graph.del_node(name),
-        order - name,  // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!?
-        command_timings)
+      new Queue(graph.del_node(name), order - name, command_timings)
 
     def dequeue(skip: String => Boolean): Option[(String, Sessions.Info)] =
     {
-      val it = order.iterator.dropWhile(name =>
-        skip(name)
-          || !graph.defined(name)  // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!?
-          || !graph.is_minimal(name))
+      val it = order.iterator.dropWhile(name => skip(name) || !graph.is_minimal(name))
       if (it.hasNext) { val name = it.next(); Some((name, graph.get_node(name))) }
       else None
     }