equal
deleted
inserted
replaced
130 { |
130 { |
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 (scale * visualizer.font_size).floor / visualizer.font_size |
135 { |
|
136 val font_height = GUI.line_metrics(visualizer.font()).getHeight.toDouble |
|
137 (scale * font_height).floor / font_height |
|
138 } |
136 |
139 |
137 def apply() = |
140 def apply() = |
138 { |
141 { |
139 val box = visualizer.Coordinates.bounding_box() |
142 val box = visualizer.Coordinates.bounding_box() |
140 val at = AffineTransform.getScaleInstance(scale_discrete, scale_discrete) |
143 val at = AffineTransform.getScaleInstance(scale_discrete, scale_discrete) |