# HG changeset patch
# User wenzelm
# Date 1420583757 -3600
# Node ID a269cc01e8eb1401133cfc3a30217abd107499cf
# Parent  7cdabe4cec33b8adae2962de4e914c09ab4766e0
clarified Vertex.Ordering, to approximate situation before 4d985afc0565, which is relevant for level arrangement;

diff -r 7cdabe4cec33 -r a269cc01e8eb src/Tools/Graphview/layout.scala
--- a/src/Tools/Graphview/layout.scala	Tue Jan 06 23:23:26 2015 +0100
+++ b/src/Tools/Graphview/layout.scala	Tue Jan 06 23:35:57 2015 +0100
@@ -27,8 +27,6 @@
     {
       def compare(v1: Vertex, v2: Vertex): Int =
         (v1, v2) match {
-          case (_: Node, _: Dummy) => -1
-          case (_: Dummy, _: Node) => 1
           case (Node(a), Node(b)) => Graph_Display.Node.Ordering.compare(a, b)
           case (Dummy(a1, a2, i), Dummy(b1, b2, j)) =>
             Graph_Display.Node.Ordering.compare(a1, b1) match {
@@ -39,6 +37,16 @@
                 }
               case ord => ord
             }
+          case (Node(a), Dummy(b, _, _)) =>
+            Graph_Display.Node.Ordering.compare(a, b) match {
+              case 0 => -1
+              case ord => ord
+            }
+          case (Dummy(a, _, _), Node(b)) =>
+            Graph_Display.Node.Ordering.compare(a, b) match {
+              case 0 => 1
+              case ord => ord
+            }
         }
     }
   }