hidpi: scale StyleSheet font sizes for better rendering of "font-size: medium|xx...

diff --git a/platform/util/src/com/intellij/util/ui/UIUtil.java b/platform/util/src/com/intellij/util/ui/UIUtil.java
index 3d5aa364d59846c338bfe857cf7bfd4aba12c614..7d19d9138691dad01d40fc0b0b576c5be86ce6d1 100644 (file)
--- a/platform/util/src/com/intellij/util/ui/UIUtil.java
+++ b/platform/util/src/com/intellij/util/ui/UIUtil.java
@@ -54,6 +54,7 @@ import javax.swing.plaf.basic.BasicComboBoxUI;
 import javax.swing.plaf.basic.BasicRadioButtonUI;
 import javax.swing.plaf.basic.ComboPopup;
 import javax.swing.text.*;
+import javax.swing.text.html.HTMLDocument;
 import javax.swing.text.html.HTMLEditorKit;
 import javax.swing.text.html.StyleSheet;
 import javax.swing.undo.UndoManager;
@@ -2369,8 +2370,19 @@ public class UIUtil {
     final StyleSheet style = new StyleSheet();
     style.addStyleSheet(isUnderDarcula() ? (StyleSheet)UIManager.getDefaults().get("StyledEditorKit.JBDefaultStyle") : DEFAULT_HTML_KIT_CSS);
     style.addRule(customCss);
+    scaleStyleSheetFontSize(style);
 
     return new HTMLEditorKit() {
+
+      @Override
+      public Document createDefaultDocument() {
+        Document document = super.createDefaultDocument();
+        if (document instanceof HTMLDocument) {
+          scaleStyleSheetFontSize(((HTMLDocument)document).getStyleSheet());
+        }
+        return document;
+      }
+
       @Override
       public StyleSheet getStyleSheet() {
         return style;
@@ -2378,6 +2390,20 @@ public class UIUtil {
     };
   }
 
+  private static void scaleStyleSheetFontSize(@Nullable StyleSheet styleSheet) {
+    if (styleSheet == null) {
+      return;
+    }
+    // 'baseFontSize' equals to javax.swing.text.html.StyleSheet.sizeMapDefault[3],
+    // where '3' == javax.swing.text.html.CSS.baseFontSizeIndex
+    // See javax.swing.text.html.StyleSheet.rebaseSizeMap()
+    int baseFontSize = 14;
+    int scaledBaseFontSize = JBUI.scaleFontSize(baseFontSize);
+    if (baseFontSize != scaledBaseFontSize) {
+      styleSheet.addRule("BASE_SIZE " + scaledBaseFontSize);
+    }
+  }
+
   public static void removeScrollBorder(final Component c) {
     for (JScrollPane scrollPane : uiTraverser(c).filter(JScrollPane.class)) {
       if (!uiParents(scrollPane, true)