equal
deleted
inserted
replaced
213 } |
213 } |
214 |
214 |
215 |
215 |
216 /* font operations */ |
216 /* font operations */ |
217 |
217 |
|
218 def copy_font(font: Font): Font = |
|
219 if (font == null) null |
|
220 else new Font(font.getFamily, font.getStyle, font.getSize) |
|
221 |
218 def line_metrics(font: Font): LineMetrics = |
222 def line_metrics(font: Font): LineMetrics = |
219 font.getLineMetrics("", new FontRenderContext(null, false, false)) |
223 font.getLineMetrics("", new FontRenderContext(null, false, false)) |
220 |
224 |
221 def imitate_font(font: Font, family: String, scale: Double = 1.0): Font = |
225 def imitate_font(font: Font, family: String, scale: Double = 1.0): Font = |
222 { |
226 { |