private static void writeFontPreferences(@NotNull String key, @NotNull Element parent, @NotNull FontPreferences preferences) {
    for (String fontFamily : preferences.getRealFontFamilies()) {
      Element element = new Element(key);
      JdomKt.addOptionTag(element, EDITOR_FONT_NAME, fontFamily);
      // Write font size as integer for compatibility
      JdomKt.addOptionTag(element, EDITOR_FONT_SIZE, String.valueOf(preferences.getSize(fontFamily)));
      parent.addContent(element);
    }
  }
private static void writeFontPreferences(@NotNull String key, @NotNull Element parent, @NotNull FontPreferences preferences)