# 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 + } } } }