# HG changeset patch
# User wenzelm
# Date 1349783871 -7200
# Node ID 083accbfa77d52ab3b9ac2b5418f1fc419038159
# Parent  84904ce4905b9dd1f1962332b421b63077ca7498
more conventional Double constants;

diff -r 84904ce4905b -r 083accbfa77d src/Tools/Graphview/src/graph_panel.scala
--- 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 {
     val padding = (4000, 2000)
     
-    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)
diff -r 84904ce4905b -r 083accbfa77d src/Tools/Graphview/src/layout_pendulum.scala
--- 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)
diff -r 84904ce4905b -r 083accbfa77d src/Tools/Graphview/src/shapes.scala
--- 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