src/Tools/GraphBrowser/graphbrowser/AWTFontMetrics.java

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/graphbrowser/AWTFontMetrics.java	Fri Jul 16 12:55:02 2021 +0200
@@ -0,0 +1,31 @@
+/***************************************************************************
+  Title:      graphbrowser/AWTFontMetrics.java
+  Author:     Gerwin Klein, TU Muenchen
+
+  AbstractFontMetrics from the AWT for graphics mode.
+  
+***************************************************************************/
+
+package isabelle.graphbrowser;
+
+import java.awt.FontMetrics;
+
+public class AWTFontMetrics implements AbstractFontMetrics {
+  private FontMetrics fontMetrics;
+
+  public AWTFontMetrics(FontMetrics m) {
+    fontMetrics = m;
+  }
+
+  public int stringWidth(String str) {
+    return fontMetrics.stringWidth(str);
+  }
+
+  public int getAscent() {
+    return fontMetrics.getAscent();
+  }
+
+  public int getDescent() {
+    return fontMetrics.getDescent();
+  }
+}