src/Pure/GUI/gui.scala
changeset 61742 fd3b214b0979
parent 61529 82fc5a6231a2
child 62113 16de2a9b5b3d
equal deleted inserted replaced
61741:adf6dd1d490e 61742:fd3b214b0979
   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   {