lib/browser/GraphBrowser/DefaultFontMetrics.java
changeset 11799 533a95523f61
child 11810 4768258b29a5
equal deleted inserted replaced
11798:fbab70de9b0d 11799:533a95523f61
       
     1 /***************************************************************************
       
     2   Title:      GraphBrowser/DefaultFontMetrics.java
       
     3   ID:         $Id$
       
     4   Author:     Stefan Berghofer, TU Muenchen
       
     5   License:    GPL (GNU GENERAL PUBLIC LICENSE)
       
     6 
       
     7   Default font metrics which is used when no graphics context
       
     8   is available.
       
     9 ***************************************************************************/
       
    10 
       
    11 package GraphBrowser;
       
    12 
       
    13 import java.awt.*;
       
    14 
       
    15 public class DefaultFontMetrics extends FontMetrics
       
    16 {
       
    17 	public DefaultFontMetrics(Font f)
       
    18 	{ super(f); }
       
    19 
       
    20 	// note : values are rather inaccurate !
       
    21 
       
    22 	public int getLeading()
       
    23 	{ return 1; }
       
    24 
       
    25 	public int getAscent()
       
    26 	{ return (int)(Math.round(font.getSize()*5.0/6.0)); }
       
    27 
       
    28 	public int getDescent()
       
    29 	{ return (int)(Math.round(font.getSize()/6.0)); }
       
    30 
       
    31 	public int stringWidth(String s)
       
    32 	{ return (int)(Math.round(s.length()*font.getSize()/2.0)); }
       
    33 }