diff -r 9cdab3186c0b -r 689868b99bde lib/browser/GraphBrowser/DefaultFontMetrics.java
--- a/lib/browser/GraphBrowser/DefaultFontMetrics.java	Wed May 07 14:53:35 2003 +0200
+++ b/lib/browser/GraphBrowser/DefaultFontMetrics.java	Wed May 07 16:38:55 2003 +0200
@@ -10,11 +10,9 @@
 
 package GraphBrowser;
 
-import java.awt.*;
+public class DefaultFontMetrics implements AbstractFontMetrics {
 
-public class DefaultFontMetrics extends FontMetrics
-{
-    protected static int[] chars =
+  private 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,
@@ -22,30 +20,30 @@
 	 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};
 
-    int size;
-
-    public DefaultFontMetrics(int size)
-    { super(null); this.size = size; }
+  private int size;
 
-    public int getLeading()
-    { return 1; }
+  public DefaultFontMetrics(int size)
+  { this.size = size; }
 
-    public int getAscent()
-    { return (int)(Math.round(size * 46.0 / 48.0)); }
-
-    public int getDescent()
-    { return (int)(Math.round(size * 10.0 / 48.0)); }
+  public int getLeading()
+  { return 1; }
 
-    public int charWidth(char c) {
-	if (c < 32 || c > 126) { return 0; }
-	else {
+  public int getAscent()
+  { return (int)(Math.round(size * 46.0 / 48.0)); }
+  
+  public int getDescent() 
+  { return (int)(Math.round(size * 10.0 / 48.0)); }
+  
+  public int charWidth(char c) {
+    if (c < 32 || c > 126) { return 0; }
+    else {
 	    return (int)(Math.round(chars[c - 32] * size / 48.0));
-	}
     }
-
-    public int stringWidth(String s) {
-	int l=0, i;
-	for (i=0; i < s.length(); i++) { l += charWidth(s.charAt(i)); }
-	return l;
-    }
+  }
+  
+  public int stringWidth(String s) {
+    int l=0, i;
+    for (i=0; i < s.length(); i++) { l += charWidth(s.charAt(i)); }
+    return l;
+  }
 }