lib/browser/GraphBrowser/DefaultFontMetrics.java
changeset 11874 83c97febc828
parent 11810 4768258b29a5
child 13968 689868b99bde
equal deleted inserted replaced
11873:38dc46b55d7e 11874:83c97febc828
    20 	 32, 35, 35, 32, 29, 37, 35, 13, 24, 32, 27, 40, 35, 37, 32, 37, 35,
    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,
    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,
    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};
    23 	 27, 24, 35, 24, 24, 24, 16, 12, 16, 28};
    24 
    24 
    25     public DefaultFontMetrics(Font f)
    25     int size;
    26     { super(f); }
    26 
       
    27     public DefaultFontMetrics(int size)
       
    28     { super(null); this.size = size; }
    27 
    29 
    28     public int getLeading()
    30     public int getLeading()
    29     { return 1; }
    31     { return 1; }
    30 
    32 
    31     public int getAscent()
    33     public int getAscent()
    32     { return (int)(Math.round(font.getSize() * 46.0 / 48.0)); }
    34     { return (int)(Math.round(size * 46.0 / 48.0)); }
    33 
    35 
    34     public int getDescent()
    36     public int getDescent()
    35     { return (int)(Math.round(font.getSize() * 10.0 / 48.0)); }
    37     { return (int)(Math.round(size * 10.0 / 48.0)); }
    36 
    38 
    37     public int charWidth(char c) {
    39     public int charWidth(char c) {
    38 	if (c < 32 || c > 126) { return 0; }
    40 	if (c < 32 || c > 126) { return 0; }
    39 	else {
    41 	else {
    40 	    return (int)(Math.round(chars[c - 32] * font.getSize() / 48.0));
    42 	    return (int)(Math.round(chars[c - 32] * size / 48.0));
    41 	}
    43 	}
    42     }
    44     }
    43 
    45 
    44     public int stringWidth(String s) {
    46     public int stringWidth(String s) {
    45 	int l=0, i;
    47 	int l=0, i;