1/***************************************************************************
2  Title:      GraphBrowser/DefaultFontMetrics.java
3  Author:     Stefan Berghofer, TU Muenchen
4  Options:    :tabSize=2:
5
6  Default font metrics which is used when no graphics context
7  is available (batch mode).
8***************************************************************************/
9
10package GraphBrowser;
11
12public class DefaultFontMetrics implements AbstractFontMetrics {
13
14  private static int[] chars =
15	{13, 13, 17, 27, 27, 43, 32, 11, 16, 16, 19, 28, 13, 28, 13, 13, 27,
16	 27, 27, 27, 27, 27, 27, 27, 27, 27, 13, 13, 28, 28, 28, 27, 49, 32,
17	 32, 35, 35, 32, 29, 37, 35, 13, 24, 32, 27, 40, 35, 37, 32, 37, 35,
18	 32, 29, 35, 32, 45, 32, 32, 29, 13, 13, 13, 22, 27, 11, 27, 27, 24,
19	 27, 27, 13, 27, 27, 11, 11, 24, 11, 40, 27, 27, 27, 27, 16, 24, 13,
20	 27, 24, 35, 24, 24, 24, 16, 12, 16, 28};
21
22  private int size;
23
24  public DefaultFontMetrics(int size)
25  { this.size = size; }
26
27  public int getLeading()
28  { return 1; }
29
30  public int getAscent()
31  { return (int)(Math.round(size * 46.0 / 48.0)); }
32
33  public int getDescent()
34  { return (int)(Math.round(size * 10.0 / 48.0)); }
35
36  public int charWidth(char c) {
37    if (c < 32 || c > 126) { return 0; }
38    else {
39	    return (int)(Math.round(chars[c - 32] * size / 48.0));
40    }
41  }
42
43  public int stringWidth(String s) {
44    int l=0, i;
45    for (i=0; i < s.length(); i++) { l += charWidth(s.charAt(i)); }
46    return l;
47  }
48}
49