# HG changeset patch # User wenzelm # Date 1355165925 -3600 # Node ID 7a2a4b84c5ee9831e9c369d5ff97d3a65b065f3f # Parent 4b0e69dc9db893e289c09d47567c97ceb6341616 tuned min/max; diff -r 4b0e69dc9db8 -r 7a2a4b84c5ee src/Tools/Graphview/src/graph_panel.scala --- 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 } } diff -r 4b0e69dc9db8 -r 7a2a4b84c5ee src/Tools/Graphview/src/layout_pendulum.scala --- 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 = diff -r 4b0e69dc9db8 -r 7a2a4b84c5ee src/Tools/Graphview/src/shapes.scala --- 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}) }