MDS/openide
1
0
Fork 0
mirror of https://gitflic.ru/project/openide/openide.git synced 2026-09-27 10:03:11 +07:00
Code Issues Packages Projects Releases Wiki Activity

Use UIUtil.getHTMLEditorKit() for correct font size scaling

Browse Source 
See IDEA-170099
This commit is contained in:
Anton Tarasov
2017-04-17 13:56:24 +03:00
parent d4e38c16b4
commit a3ac0e0532
2 changed files with 2 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files
platform/platform-impl/src/com/intellij/ide/plugins/PluginManagerMain.java
+1 -1
View File
@@ -139,7 +139,7 @@ public abstract class PluginManagerMain implements Disposable {
protected void init() {
GuiUtils.replaceJSplitPaneWithIDEASplitter(main, true);
HTMLEditorKit kit = new HTMLEditorKit();
HTMLEditorKit kit = UIUtil.getHTMLEditorKit();
StyleSheet sheet = kit.getStyleSheet();
sheet.addRule("ul {margin-left: 16px}"); // list-style-type: none;
myDescriptionTextArea.setEditorKit(kit);
platform/platform-impl/src/com/intellij/openapi/updateSettings/impl/DetectedPluginsPanel.java
+1 -1
View File
@@ -96,7 +96,7 @@ public class DetectedPluginsPanel extends OrderPanel<PluginDownloader> {
setCheckboxColumnName("");
myDescriptionPanel.setPreferredSize(new Dimension(400, -1));
myDescriptionPanel.setEditable(false);
myDescriptionPanel.setContentType(UIUtil.HTML_MIME);
myDescriptionPanel.setEditorKit(UIUtil.getHTMLEditorKit());
myDescriptionPanel.addHyperlinkListener(new PluginManagerMain.MyHyperlinkListener());
removeAll();