--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/graphbrowser/AbstractFontMetrics.java Fri Jul 16 12:55:02 2021 +0200
@@ -0,0 +1,16 @@
+/***************************************************************************
+ Title: graphbrowser/AWTFontMetrics.java
+ Author: Gerwin Klein, TU Muenchen
+
+ AbstractFontMetrics avoids dependency on java.awt.FontMetrics in
+ batch mode.
+
+***************************************************************************/
+
+package isabelle.graphbrowser;
+
+public interface AbstractFontMetrics {
+ public int stringWidth(String str);
+ public int getAscent();
+ public int getDescent();
+}