src/Tools/Graphview/graph_panel.scala
changeset 59287 9d4728e00925
parent 59286 ac74eedb910a
child 59290 569a8109eeb2
equal deleted inserted replaced
59286:ac74eedb910a 59287:9d4728e00925
   131       _scale = (s min 10.0) max 0.1
   131       _scale = (s min 10.0) max 0.1
   132     }
   132     }
   133 
   133 
   134     def scale_discrete: Double =
   134     def scale_discrete: Double =
   135     {
   135     {
   136       val font_height = GUI.line_metrics(visualizer.font()).getHeight.toDouble
   136       val font_height = GUI.line_metrics(visualizer.font()).getHeight.toInt
   137       (scale * font_height).floor / font_height
   137       (scale * font_height).floor / font_height
   138     }
   138     }
   139 
   139 
   140     def apply() =
   140     def apply() =
   141     {
   141     {