public void setFont(String fontName, int fontSize) {
		this.fontMetrics = new SystemFontMetrics(fontName);
		this.fontName = fontMetrics.getFont().getPSName();
		this.fontSize = fontSize;

		String psname = POSTSCRIPT_FONT_NAMES.get(this.fontName);
		if (psname == null) {
			psname = this.fontName;
		}

		ps.append(String.format(Locale.US, "/%s findfont %d scalefont setfont\n", psname, fontSize));
	}
Compute the header separately because we need to wait for the bounding box
tool/src/org/antlr/v4/gui/PostScriptDocument.java