src/Tools/Graphview/src/graph_panel.scala

   fit_to_window()
   
   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)
                   paint_panel.set_preferred_size()
                 }

         scale = 1
       else {
         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)
       }
     }
     
     def pane_to_graph_coordinates(at: Point2D): Point2D = {

         case KeyTyped(_, c, m, _) => typed(c, m)
       }      
       
       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', _) => {
           Transform.fit_to_window()
         }

       }
 
       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)
         val r = panel.peer.getViewport.getViewRect
         val (width, height) = (r.getWidth, r.getHeight)