src/Tools/Graphview/src/visualizer.scala
changeset 50467 4b0e69dc9db8
parent 50465 0afb01666df2
child 50470 cb73e91bb019
--- a/src/Tools/Graphview/src/visualizer.scala	Mon Dec 10 19:28:56 2012 +0100
+++ b/src/Tools/Graphview/src/visualizer.scala	Mon Dec 10 19:42:58 2012 +0100
@@ -46,7 +46,7 @@
         case None =>
         case Some(ds) =>
           dummies += (e ->
-            (ds.zipWithIndex :\ List[(Double, Double)]()) {
+            (ds.zipWithIndex :\ List.empty[(Double, Double)]) {
               case ((t, i), n) => if (index == i) to :: n else t :: n
             }
           )
@@ -68,7 +68,7 @@
 
     def layout()
     {
-      val (l, d) = Layout_Pendulum(model.current)
+      val (l, d) = Layout_Pendulum(model.current)  // FIXME avoid computation on Swing thread
       nodes = l
       dummies = d
     }