|
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 |
|
10 package isabelle.graphbrowser; |
|
11 |
|
12 public 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 } |