lib/browser/GraphBrowser/DefaultFontMetrics.java
changeset 11810 4768258b29a5
parent 11799 533a95523f61
child 11874 83c97febc828
equal deleted inserted replaced
11809:c9ffdd63dd93 11810:4768258b29a5
    12 
    12 
    13 import java.awt.*;
    13 import java.awt.*;
    14 
    14 
    15 public class DefaultFontMetrics extends FontMetrics
    15 public class DefaultFontMetrics extends FontMetrics
    16 {
    16 {
    17 	public DefaultFontMetrics(Font f)
    17     protected static int[] chars =
    18 	{ super(f); }
    18 	{13, 13, 17, 27, 27, 43, 32, 11, 16, 16, 19, 28, 13, 28, 13, 13, 27,
       
    19 	 27, 27, 27, 27, 27, 27, 27, 27, 27, 13, 13, 28, 28, 28, 27, 49, 32,
       
    20 	 32, 35, 35, 32, 29, 37, 35, 13, 24, 32, 27, 40, 35, 37, 32, 37, 35,
       
    21 	 32, 29, 35, 32, 45, 32, 32, 29, 13, 13, 13, 22, 27, 11, 27, 27, 24,
       
    22 	 27, 27, 13, 27, 27, 11, 11, 24, 11, 40, 27, 27, 27, 27, 16, 24, 13,
       
    23 	 27, 24, 35, 24, 24, 24, 16, 12, 16, 28};
    19 
    24 
    20 	// note : values are rather inaccurate !
    25     public DefaultFontMetrics(Font f)
       
    26     { super(f); }
    21 
    27 
    22 	public int getLeading()
    28     public int getLeading()
    23 	{ return 1; }
    29     { return 1; }
    24 
    30 
    25 	public int getAscent()
    31     public int getAscent()
    26 	{ return (int)(Math.round(font.getSize()*5.0/6.0)); }
    32     { return (int)(Math.round(font.getSize() * 46.0 / 48.0)); }
    27 
    33 
    28 	public int getDescent()
    34     public int getDescent()
    29 	{ return (int)(Math.round(font.getSize()/6.0)); }
    35     { return (int)(Math.round(font.getSize() * 10.0 / 48.0)); }
    30 
    36 
    31 	public int stringWidth(String s)
    37     public int charWidth(char c) {
    32 	{ return (int)(Math.round(s.length()*font.getSize()/2.0)); }
    38 	if (c < 32 || c > 126) { return 0; }
       
    39 	else {
       
    40 	    return (int)(Math.round(chars[c - 32] * font.getSize() / 48.0));
       
    41 	}
       
    42     }
       
    43 
       
    44     public int stringWidth(String s) {
       
    45 	int l=0, i;
       
    46 	for (i=0; i < s.length(); i++) { l += charWidth(s.charAt(i)); }
       
    47 	return l;
       
    48     }
    33 }
    49 }