--- a/src/isabelle/LocaleBrowser/shapes.scala	Thu Aug 30 17:22:22 2012 +0200
+++ b/src/isabelle/LocaleBrowser/shapes.scala	Thu Aug 30 17:35:45 2012 +0200
@@ -111,6 +111,59 @@
     }
   }
   
+  object Cardinal_Spline_Edge extends Edge {
+    private val stroke = new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
+    private val slack = 0.12
+
+    def paint(g: Graphics2D, vis: Visualizer, peer: (String, String)) {
+      val ((fx, fy), (tx, ty)) = (vis.Coordinates(peer._1), vis.Coordinates(peer._2))
+      val dummies = {
+        val (min, max) = (math.min(fy, ty), math.max(fy, ty))
+        
+        vis.Coordinates(peer).filter({case (_, y) => y > min && y < max})
+      }
+      
+      if (dummies.isEmpty) Straight_Edge.paint(g, vis, peer)
+      else {
+        val path = new GeneralPath(Path2D.WIND_EVEN_ODD, dummies.length + 2)
+        path.moveTo(fx, fy)
+        
+        val coords = ((fx, fy) :: dummies ::: List((tx, ty)))
+        val (dx, dy) = (coords(2)._1 - coords(0)._1, coords(2)._2 - coords(0)._2)
+        
+        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) 
+              (dx2, dy2)
+            }
+          })
+      
+        val (lx, ly) = dummies.last
+        path.curveTo(lx + slack * dx2, ly + slack * dy2,
+                     tx - slack * dx2, ty - slack * dy2,
+                     tx              , ty)
+        
+        dummies.foreach({
+            case (x, y) => {
+              val at = AffineTransform.getTranslateInstance(x, y)
+              Dummy.paint_transformed(g, vis, None, at)
+            }
+          })      
+
+        g.setStroke(stroke)
+        g.setColor(vis.Color(peer))
+        g.draw(path)
+
+        Arrow_Head.paint(g, path, vis.Drawer.shape(g, Some(peer._2)))        
+      }
+    }    
+  }
+  
   object Arrow_Head {
     type Point = (Double, Double)
     

--- a/src/isabelle/LocaleBrowser/visualizer.scala	Thu Aug 30 17:22:22 2012 +0200
+++ b/src/isabelle/LocaleBrowser/visualizer.scala	Thu Aug 30 17:35:45 2012 +0200
@@ -79,7 +79,7 @@
     }
     
     def apply(g: Graphics2D, e: (String, String)) = {
-      Straight_Edge.paint(g, visualizer, e)
+      Cardinal_Spline_Edge.paint(g, visualizer, e)
     }
     
     def shape(g: Graphics2D, n: Option[String]): Shape = n match {