# HG changeset patch
# User wenzelm
# Date 1355164978 -3600
# Node ID 4b0e69dc9db893e289c09d47567c97ceb6341616
# Parent  53d3930dae0c0cb9fcc75044b9d7915d1bbb28e7
tuned;

diff -r 53d3930dae0c -r 4b0e69dc9db8 src/Tools/Graphview/src/layout_pendulum.scala
--- a/src/Tools/Graphview/src/layout_pendulum.scala	Mon Dec 10 19:28:56 2012 +0100
+++ b/src/Tools/Graphview/src/layout_pendulum.scala	Mon Dec 10 19:42:58 2012 +0100
@@ -28,12 +28,12 @@
   def apply(graph: Model.Graph): Layout =
   {
     if (graph.is_empty)
-      (Map[Key, Point](), Map[(Key, Key), List[Point]]())
+      (Map.empty[Key, Point], Map.empty[(Key, Key), List[Point]])
     else {
       val initial_levels = level_map(graph)
 
       val (dummy_graph, dummies, dummy_levels) =
-        ((graph, Map[(Key, Key), List[Key]](), initial_levels) /: graph.keys) {
+        ((graph, Map.empty[(Key, Key), List[Key]], initial_levels) /: graph.keys) {
           case ((graph, dummies, levels), from) =>
             ((graph, dummies, levels) /: graph.imm_succs(from)) {
               case ((graph, dummies, levels), to) =>
@@ -58,7 +58,7 @@
         )
 
       val dummy_coords =
-        (Map[(Key, Key), List[Point]]() /: dummies.keys) {
+        (Map.empty[(Key, Key), List[Point]] /: dummies.keys) {
           case (map, key) => map + (key -> dummies(key).map(coords(_)))
         }
 
@@ -87,7 +87,7 @@
   }
 
   def level_map(graph: Model.Graph): Map[Key, Int] = 
-    (Map[Key, Int]() /: graph.topological_order) {
+    (Map.empty[Key, Int] /: graph.topological_order) {
       (levels, key) => {
         val lev = 1 + (-1 /: graph.imm_preds(key)) { case (m, key) => m max levels(key) }
         levels + (key -> lev)
@@ -163,7 +163,7 @@
   }
   
   def initial_coordinates(levels: Levels): Coordinates =
-    (Map[Key, Point]() /: levels.zipWithIndex){
+    (Map.empty[Key, Point] /: levels.zipWithIndex){
       case (coords, (level, yi)) =>
         (coords /: level.zipWithIndex) {
           case (coords, (node, xi)) => 
@@ -180,7 +180,7 @@
                   top_down: Boolean): (Regions, Coordinates, Boolean) =
     { 
       val (nextr, nextc, moved) = 
-      ((List[List[Region]](), coords, false) /:
+      ((List.empty[List[Region]], coords, false) /:
        (if (top_down) regions else regions.reverse)) {
         case ((tops, coords, prev_moved), bot) => {
             val nextb = collapse(coords, bot, top_down)
diff -r 53d3930dae0c -r 4b0e69dc9db8 src/Tools/Graphview/src/model.scala
--- a/src/Tools/Graphview/src/model.scala	Mon Dec 10 19:28:56 2012 +0100
+++ b/src/Tools/Graphview/src/model.scala	Mon Dec 10 19:42:58 2012 +0100
@@ -88,12 +88,12 @@
         }
       }
     
-  private var _colors = Map[String, Color]()
+  private var _colors = Map.empty[String, Color]
   def colors = _colors
   
   private def build_colors() {
     _colors = 
-      (Map[String, Color]() /: Colors()) ({
+      (Map.empty[String, Color] /: Colors()) ({
           case (colors, (enabled, color, mutator)) => {
               (colors /: mutator.mutate(graph, graph).keys) ({
                   case (colors, k) => colors + (k -> color)
diff -r 53d3930dae0c -r 4b0e69dc9db8 src/Tools/Graphview/src/mutator_dialog.scala
--- a/src/Tools/Graphview/src/mutator_dialog.scala	Mon Dec 10 19:28:56 2012 +0100
+++ b/src/Tools/Graphview/src/mutator_dialog.scala	Mon Dec 10 19:42:58 2012 +0100
@@ -164,7 +164,7 @@
     private val (_enabled, _color, _mutator) = initials
     
     private val inputs: List[(String, Mutator_Input_Value)] = get_Inputs()
-    var focusList = List[java.awt.Component]()
+    var focusList = List.empty[java.awt.Component]
     private val enabledBox = new iCheckBox("Enabled", _enabled)
 
     border = new EmptyBorder(5, 5, 5, 5)
diff -r 53d3930dae0c -r 4b0e69dc9db8 src/Tools/Graphview/src/shapes.scala
--- a/src/Tools/Graphview/src/shapes.scala	Mon Dec 10 19:28:56 2012 +0100
+++ b/src/Tools/Graphview/src/shapes.scala	Mon Dec 10 19:42:58 2012 +0100
@@ -8,20 +8,24 @@
 
 
 import java.awt.{BasicStroke, Graphics2D, Shape}
-import java.awt.geom.{AffineTransform, GeneralPath, Path2D, Rectangle2D}
+import java.awt.geom.{AffineTransform, GeneralPath, Path2D, Rectangle2D, PathIterator}
 
 
-object Shapes {
-  trait Node {
+object Shapes
+{
+  trait Node
+  {
     def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Shape
     def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Unit
   }
 
-  object Growing_Node extends Node {
+  object Growing_Node extends Node
+  {
     private val stroke =
       new BasicStroke(3, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
 
-    def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Rectangle2D.Double = {
+    def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Rectangle2D.Double =
+    {
       val caption = visualizer.Caption(peer.get)
       val bounds = g.getFontMetrics.getStringBounds(caption, g)
       val (x, y) = visualizer.Coordinates(peer.get)
@@ -34,7 +38,8 @@
       )
     }
 
-    def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String]) {
+    def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String])
+    {
       val caption = visualizer.Caption(peer.get)
       val bounds = g.getFontMetrics.getStringBounds(caption, g)
       val s = shape(g, visualizer, peer)
@@ -47,13 +52,13 @@
       g.fill(s)
       g.setColor(foreground)
       g.drawString(caption,
-                   (s.getCenterX + (-bounds.getWidth / 2)).toFloat,
-                   (s.getCenterY + 5).toFloat
-                  )
+        (s.getCenterX + (- bounds.getWidth / 2)).toFloat,
+        (s.getCenterY + 5).toFloat)
     }
   }
 
-  object Dummy extends Node {
+  object Dummy extends Node
+  {
     private val stroke =
       new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
     private val shape = new Rectangle2D.Double(-8, -8, 16, 16)
@@ -63,9 +68,9 @@
 
     def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Unit =
       paint_transformed(g, visualizer, peer, identity)
-    
+
     def paint_transformed(g: Graphics2D, visualizer: Visualizer,
-                          peer: Option[String], at: AffineTransform)
+      peer: Option[String], at: AffineTransform)
     {
       val (border, background, foreground) = visualizer.Color(peer)
       g.setStroke(stroke)
@@ -74,24 +79,24 @@
     }
   }
 
-  trait Edge {
-    def paint(g: Graphics2D, visualizer: Visualizer, peer: (String, String),
-              head: Boolean, dummies: Boolean)
+  trait Edge
+  {
+    def paint(g: Graphics2D, visualizer: Visualizer,
+      peer: (String, String), head: Boolean, dummies: Boolean)
   }
 
-  object Straight_Edge extends Edge {  
+  object Straight_Edge extends Edge
+  {
     private val stroke =
       new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
 
     def paint(g: Graphics2D, visualizer: Visualizer,
-              peer: (String, String), head: Boolean, dummies: Boolean)
+      peer: (String, String), head: Boolean, dummies: Boolean)
     {
-      val ((fx, fy), (tx, ty)) =
-        (visualizer.Coordinates(peer._1), visualizer.Coordinates(peer._2))
+      val ((fx, fy), (tx, ty)) = (visualizer.Coordinates(peer._1), visualizer.Coordinates(peer._2))
       val ds = {
         val (min, max) = (math.min(fy, ty), math.max(fy, ty))
-        
-        visualizer.Coordinates(peer).filter({case (_, y) => y > min && y < max})
+        visualizer.Coordinates(peer).filter({ case (_, y) => y > min && y < max })
       }
       val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
 
@@ -107,56 +112,57 @@
             }
           })
       }
-      
+
       g.setStroke(stroke)
       g.setColor(visualizer.Color(peer))
       g.draw(path)
-      
+
       if (head) Arrow_Head.paint(g, path, visualizer.Drawer.shape(g, Some(peer._2)))
     }
   }
-  
-  object Cardinal_Spline_Edge extends Edge {
+
+  object Cardinal_Spline_Edge extends Edge
+  {
     private val stroke =
       new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
     private val slack = 0.1
 
     def paint(g: Graphics2D, visualizer: Visualizer,
-              peer: (String, String), head: Boolean, dummies: Boolean)
+      peer: (String, String), head: Boolean, dummies: Boolean)
     {
       val ((fx, fy), (tx, ty)) =
         (visualizer.Coordinates(peer._1), visualizer.Coordinates(peer._2))
       val ds = {
         val (min, max) = (math.min(fy, ty), math.max(fy, ty))
-        
+
         visualizer.Coordinates(peer).filter({case (_, y) => y > min && y < max})
       }
-      
+
       if (ds.isEmpty) Straight_Edge.paint(g, visualizer, peer, head, dummies)
       else {
         val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
         path.moveTo(fx, fy)
-        
+
         val coords = ((fx, fy) :: ds ::: List((tx, ty)))
         val (dx, dy) = (coords(2)._1 - coords(0)._1, coords(2)._2 - coords(0)._2)
-        
-        val (dx2, dy2) = 
+
+        val (dx2, dy2) =
           ((dx, dy) /: coords.sliding(3))({
             case ((dx, dy), List((lx, ly), (mx, my), (rx, ry))) => {
               val (dx2, dy2) = (rx - lx, ry - ly)
 
               path.curveTo(lx + slack * dx , ly + slack * dy,
                            mx - slack * dx2, my - slack * dy2,
-                           mx              , my) 
+                           mx              , my)
               (dx2, dy2)
             }
           })
-      
+
         val (lx, ly) = ds.last
         path.curveTo(lx + slack * dx2, ly + slack * dy2,
                      tx - slack * dx2, ty - slack * dy2,
                      tx              , ty)
-        
+
         if (dummies) {
           ds.foreach({
               case (x, y) => {
@@ -170,20 +176,19 @@
         g.setColor(visualizer.Color(peer))
         g.draw(path)
 
-        if (head) Arrow_Head.paint(g, path, visualizer.Drawer.shape(g, Some(peer._2)))        
+        if (head) Arrow_Head.paint(g, path, visualizer.Drawer.shape(g, Some(peer._2)))
       }
-    }    
+    }
   }
-  
-  object Arrow_Head {
+
+  object Arrow_Head
+  {
     type Point = (Double, Double)
-    
-    private def position(path: GeneralPath,
-                         shape: Shape): Option[AffineTransform] = {
-      def intersecting_line(path: GeneralPath,
-                            shape: Shape): Option[(Point, Point)] = {
-        import java.awt.geom.PathIterator
 
+    private def position(path: GeneralPath, shape: Shape): Option[AffineTransform] =
+    {
+      def intersecting_line(path: GeneralPath, shape: Shape): Option[(Point, Point)] =
+      {
         val i = path.getPathIterator(null, 1.0)
         var seg = Array[Double](0,0,0,0,0,0)
         var p1 = (0.0, 0.0)
@@ -191,23 +196,21 @@
         while (!i.isDone()) {
           i.currentSegment(seg) match {
             case PathIterator.SEG_MOVETO => p2 = (seg(0), seg(1))
-            case PathIterator.SEG_LINETO => {
-                p1 = p2
-                p2 = (seg(0), seg(1))
+            case PathIterator.SEG_LINETO =>
+              p1 = p2
+              p2 = (seg(0), seg(1))
 
-                if(shape.contains(seg(0), seg(1)))
-                  return Some((p1, p2))
-            }
+              if(shape.contains(seg(0), seg(1)))
+                return Some((p1, p2))
             case _ =>
           }
           i.next()
         }
+        None
+      }
 
-        None
-      }      
-      
-      def binary_search(line: (Point, Point),
-                        shape: Shape): Option[AffineTransform] = {
+      def binary_search(line: (Point, Point), shape: Shape): Option[AffineTransform] =
+      {
         val ((fx, fy), (tx, ty)) = line
         if (shape.contains(fx, fy) == shape.contains(tx, ty))
           None
@@ -217,7 +220,8 @@
             val at = AffineTransform.getTranslateInstance(fx, fy)
             at.rotate(- (math.atan2(dx, dy) + math.Pi / 2))
             Some(at)
-          } else {
+          }
+          else {
             val (mx, my) = (fx + (tx - fx) / 2.0, fy + (ty - fy) / 2.0)
             if (shape.contains(fx, fy) == shape.contains(mx, my))
               binary_search(((mx, my), (tx, ty)), shape)
@@ -226,13 +230,13 @@
           }
         }
       }
-      
+
       intersecting_line(path, shape) match {
         case None => None
         case Some(line) => binary_search(line, shape)
       }
     }
-    
+
     def paint(g: Graphics2D, path: GeneralPath, shape: Shape)
     {
       position(path, shape) match {
@@ -246,7 +250,7 @@
           arrow.lineTo(0, 0)
           arrow.transform(at)
 
-          g.fill(arrow)            
+          g.fill(arrow)
         }
       }
     }
diff -r 53d3930dae0c -r 4b0e69dc9db8 src/Tools/Graphview/src/visualizer.scala
--- 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
     }