tuned min/max;

--- a/src/Tools/Graphview/src/graph_panel.scala	Mon Dec 10 19:42:58 2012 +0100
+++ b/src/Tools/Graphview/src/graph_panel.scala	Mon Dec 10 19:58:45 2012 +0100
@@ -115,10 +115,11 @@
     
     private var _scale = 1.0
     def scale = _scale
-    def scale_= (s: Double) = {
-                  _scale = math.max(math.min(s, 10), 0.01)
-                  paint_panel.set_preferred_size()
-                }
+    def scale_= (s: Double) =
+    {
+      _scale = (s min 10) max 0.01
+      paint_panel.set_preferred_size()
+    }
                 
     def apply() = {
       val (minX, minY, _, _) = visualizer.Coordinates.bounds()
@@ -136,7 +137,7 @@
 
         val (dx, dy) = (maxX - minX + padding._1, maxY - minY + padding._2)
         val (sx, sy) = (1.0 * size.width / dx, 1.0 * size.height / dy)
-        scale = math.min(sx, sy)
+        scale = sx min sy
       }
     }
     

--- a/src/Tools/Graphview/src/layout_pendulum.scala	Mon Dec 10 19:42:58 2012 +0100
+++ b/src/Tools/Graphview/src/layout_pendulum.scala	Mon Dec 10 19:58:45 2012 +0100
@@ -132,9 +132,7 @@
       child.map(k => {
           val ps = if (top_down) graph.imm_preds(k) else graph.imm_succs(k)
           val weight = 
-            (0.0 /: ps) {
-              (w, p) => w + math.max(0, parent.indexOf(p))
-            } / math.max(ps.size, 1)
+            (0.0 /: ps) { (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1)
           (k, weight)
       }).sortBy(_._2).map(_._1)
     
@@ -232,11 +230,11 @@
               else if (i == level.length - 1 && d >= 0) d
               else if (d < 0) {
                 val prev = level(i-1)
-                math.max( -(r.distance(coords, prev) - x_distance), d )
+                (-(r.distance(coords, prev) - x_distance)) max d
               }
               else {
                 val next = level(i+1)
-                math.min( r.distance(coords, next) - x_distance, d )
+                (r.distance(coords, next) - x_distance) min d
               }
             }
             
@@ -264,14 +262,14 @@
     def right(coords: Coordinates): Double =
       nodes.map(coords(_)._1).max
     def distance(coords: Coordinates, to: Region): Double =
-      math.min(math.abs(left(coords) - to.left(coords)),
-               math.abs(right(coords) - to.right(coords)))
+      math.abs(left(coords) - to.left(coords)) min
+      math.abs(right(coords) - to.right(coords))
     
     def deflection(coords: Coordinates, use_preds: Boolean) = 
       nodes.map(k => (coords(k)._1,
                       if (use_preds) graph.imm_preds(k).toList  // FIXME iterator
                       else graph.imm_succs(k).toList))
-      .map({case (x, as) => as.map(coords(_)._1 - x).sum / math.max(as.length, 1)})
+      .map({ case (x, as) => as.map(coords(_)._1 - x).sum / (as.length max 1) })
       .sum / nodes.length
     
     def move(coords: Coordinates, by: Double): Coordinates = 

--- a/src/Tools/Graphview/src/shapes.scala	Mon Dec 10 19:42:58 2012 +0100
+++ b/src/Tools/Graphview/src/shapes.scala	Mon Dec 10 19:58:45 2012 +0100
@@ -94,8 +94,10 @@
       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))
+      val ds =
+      {
+        val min = fy min ty
+        val max = fy max ty
         visualizer.Coordinates(peer).filter({ case (_, y) => y > min && y < max })
       }
       val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
@@ -132,9 +134,10 @@
     {
       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))
-
+      val ds =
+      {
+        val min = fy min ty
+        val max = fy max ty
         visualizer.Coordinates(peer).filter({case (_, y) => y > min && y < max})
       }