author wenzelm Tue, 09 Oct 2012 13:57:51 +0200 changeset 49745 083accbfa77d parent 49744 84904ce4905b child 49746 5073cb632b6c
more conventional Double constants;
```--- a/src/Tools/Graphview/src/graph_panel.scala	Tue Oct 09 13:50:24 2012 +0200
+++ b/src/Tools/Graphview/src/graph_panel.scala	Tue Oct 09 13:57:51 2012 +0200
@@ -112,7 +112,7 @@
protected object Transform {

-    private var _scale = 1d
+    private var _scale = 1.0
def scale = _scale
def scale_= (s: Double) = {
_scale = math.max(math.min(s, 10), 0.01)
@@ -134,7 +134,7 @@
val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds()

val (dx, dy) = (maxX - minX + padding._1, maxY - minY + padding._2)
-        val (sx, sy) = (1d * size.width / dx, 1d * size.height / dy)
+        val (sx, sy) = (1.0 * size.width / dx, 1.0 * size.height / dy)
scale = math.min(sx, sy)
}
}
@@ -158,11 +158,11 @@

def typed(c: Char, m: Modifiers) = (c, m) match {
case ('+', _) => {
-          Transform.scale *= 5d/4
+          Transform.scale *= 5.0/4
}

case ('-', _) => {
-          Transform.scale *= 4d/5
+          Transform.scale *= 4.0/5
}

case ('0', _) => {
@@ -283,7 +283,7 @@
def wheel(rotation: Int, at: Point) {
val at2 = Transform.pane_to_graph_coordinates(at)
// > 0 -> up
-        Transform.scale *= (if (rotation > 0) 4d/5 else 5d/4)
+        Transform.scale *= (if (rotation > 0) 4.0/5 else 5.0/4)

// move mouseposition to center
Transform().transform(at2, at2)```
```--- a/src/Tools/Graphview/src/layout_pendulum.scala	Tue Oct 09 13:50:24 2012 +0200
+++ b/src/Tools/Graphview/src/layout_pendulum.scala	Tue Oct 09 13:57:51 2012 +0200
@@ -126,12 +126,13 @@
levels.sliding(2).map(in_level).sum
}

-  def minimize_crossings(graph: Model.Graph, levels: Levels): Levels = {
+  def minimize_crossings(graph: Model.Graph, levels: Levels): Levels =
+  {
def resort_level(parent: Level, child: Level, top_down: Boolean): Level =
child.map(k => {
val ps = if (top_down) graph.imm_preds(k) else graph.imm_succs(k)
val weight =
-            (0d /: ps) {
+            (0.0 /: ps) {
(w, p) => w + math.max(0, parent.indexOf(p))
} / math.max(ps.size, 1)
(k, weight)```
```--- a/src/Tools/Graphview/src/shapes.scala	Tue Oct 09 13:50:24 2012 +0200
+++ b/src/Tools/Graphview/src/shapes.scala	Tue Oct 09 13:57:51 2012 +0200
@@ -181,10 +181,10 @@
shape: Shape): Option[(Point, Point)] = {
import java.awt.geom.PathIterator

-        val i = path.getPathIterator(null, 1d)
+        val i = path.getPathIterator(null, 1.0)
var seg = Array[Double](0,0,0,0,0,0)
-        var p1 = (0d, 0d)
-        var p2 = (0d, 0d)
+        var p1 = (0.0, 0.0)
+        var p2 = (0.0, 0.0)
while (!i.isDone()) {
i.currentSegment(seg) match {
case PathIterator.SEG_MOVETO => p2 = (seg(0), seg(1))
@@ -210,12 +210,12 @@
None
else {
val (dx, dy) = (fx - tx, fy - ty)
-          if ( (dx * dx + dy * dy) < 1d ) {
+          if ((dx * dx + dy * dy) < 1.0) {
val at = AffineTransform.getTranslateInstance(fx, fy)
at.rotate(- (math.atan2(dx, dy) + math.Pi / 2))
Some(at)
} else {
-            val (mx, my) = (fx + (tx - fx) / 2d, fy + (ty - fy) / 2d)
+            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)
else```