lib/browser/GraphBrowser/DefaultFontMetrics.java

--- a/lib/browser/GraphBrowser/DefaultFontMetrics.java	Tue Oct 16 17:58:13 2001 +0200
+++ b/lib/browser/GraphBrowser/DefaultFontMetrics.java	Tue Oct 16 19:53:12 2001 +0200
@@ -14,20 +14,36 @@
 
 public class DefaultFontMetrics extends FontMetrics
 {
-	public DefaultFontMetrics(Font f)
-	{ super(f); }
+    protected static int[] chars =
+	{13, 13, 17, 27, 27, 43, 32, 11, 16, 16, 19, 28, 13, 28, 13, 13, 27,
+	 27, 27, 27, 27, 27, 27, 27, 27, 27, 13, 13, 28, 28, 28, 27, 49, 32,
+	 32, 35, 35, 32, 29, 37, 35, 13, 24, 32, 27, 40, 35, 37, 32, 37, 35,
+	 32, 29, 35, 32, 45, 32, 32, 29, 13, 13, 13, 22, 27, 11, 27, 27, 24,
+	 27, 27, 13, 27, 27, 11, 11, 24, 11, 40, 27, 27, 27, 27, 16, 24, 13,
+	 27, 24, 35, 24, 24, 24, 16, 12, 16, 28};
 
-	// note : values are rather inaccurate !
+    public DefaultFontMetrics(Font f)
+    { super(f); }
 
-	public int getLeading()
-	{ return 1; }
+    public int getLeading()
+    { return 1; }
+
+    public int getAscent()
+    { return (int)(Math.round(font.getSize() * 46.0 / 48.0)); }
 
-	public int getAscent()
-	{ return (int)(Math.round(font.getSize()*5.0/6.0)); }
+    public int getDescent()
+    { return (int)(Math.round(font.getSize() * 10.0 / 48.0)); }
 
-	public int getDescent()
-	{ return (int)(Math.round(font.getSize()/6.0)); }
+    public int charWidth(char c) {
+	if (c < 32 || c > 126) { return 0; }
+	else {
+	    return (int)(Math.round(chars[c - 32] * font.getSize() / 48.0));
+	}
+    }
 
-	public int stringWidth(String s)
-	{ return (int)(Math.round(s.length()*font.getSize()/2.0)); }
+    public int stringWidth(String s) {
+	int l=0, i;
+	for (i=0; i < s.length(); i++) { l += charWidth(s.charAt(i)); }
+	return l;
+    }
 }