updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
proper update of jEdit environment -- avoid warnings in Java 11;
activate jdk-11+28;
/***************************************************************************
Title: GraphBrowser/AWTFontMetrics.java
Author: Gerwin Klein, TU Muenchen
AbstractFontMetrics from the AWT for graphics mode.
***************************************************************************/
package 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();
}
}