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

IDEA-120011 quick documentation looses styling

Browse Source
This commit is contained in:
Gregory.Shrago
2014-03-27 19:56:21 +04:00
parent 64f0a141ed
commit 07df0a4cc2
2 changed files with 29 additions and 12 deletions
Download Patch File Download Diff File Expand all files Collapse all files
platform/platform-impl/src/com/intellij/ide/util/TipUIUtil.java
+11 -6
View File
@@ -205,8 +205,6 @@ public class TipUIUtil {
public static JEditorPane createTipBrowser() {
JEditorPane browser = new JEditorPane();
browser.setEditable(false);
HTMLEditorKit editorKit = new HTMLEditorKit();
browser.setEditorKit(editorKit);
browser.setBackground(UIUtil.getTextFieldBackground());
browser.addHyperlinkListener(
new HyperlinkListener() {
@@ -217,16 +215,23 @@ public class TipUIUtil {
}
}
);
HTMLEditorKit kit;
try {
// set default CSS for plugin tips
URL resource = ResourceUtil.getResource(TipUIUtil.class, "/tips/css/", UIUtil.isUnderDarcula() ? "tips_darcula.css" : "tips.css");
StyleSheet sheet = new StyleSheet();
sheet.loadRules(new InputStreamReader(resource.openStream()), resource);
editorKit.setStyleSheet(sheet);
final StyleSheet styleSheet = new StyleSheet();
styleSheet.loadRules(new InputStreamReader(resource.openStream()), resource);
kit = new HTMLEditorKit() {
@Override
public StyleSheet getStyleSheet() {
return styleSheet;
}
};
}
catch (IOException ignored) {
kit = new HTMLEditorKit();
}
browser.setEditorKit(kit);
return browser;
}
}
platform/util/src/com/intellij/util/ui/UIUtil.java
+18 -6
View File
@@ -72,6 +72,15 @@ import java.util.regex.Pattern;
public class UIUtil {
@NonNls public static final String BORDER_LINE = "<hr size=1 noshade>";
private static final StyleSheet DEFAULT_HTML_KIT_CSS;
static {
// save the default JRE CSS and ..
HTMLEditorKit kit = new HTMLEditorKit();
DEFAULT_HTML_KIT_CSS = kit.getStyleSheet();
// .. erase global ref to this CSS so no one can alter it
kit.setStyleSheet(null);
}
public static int getMultiClickInterval() {
Object property = Toolkit.getDefaultToolkit().getDesktopProperty("awt.multiClickInterval");
@@ -1906,17 +1915,20 @@ public class UIUtil {
}
public static HTMLEditorKit getHTMLEditorKit() {
final HTMLEditorKit kit = new HTMLEditorKit();
Font font = getLabelFont();
@NonNls String family = font != null ? font.getFamily() : "Tahoma";
int size = font != null ? font.getSize() : 11;
final StyleSheet styleSheet = kit.getStyleSheet();
styleSheet.addRule(String.format("body, div, p { font-family: %s; font-size: %s; } p { margin-top: 0; }", family, size));
kit.setStyleSheet(styleSheet);
final StyleSheet style = new StyleSheet();
style.addStyleSheet(DEFAULT_HTML_KIT_CSS);
style.addRule(String.format("body, div, p { font-family: %s; font-size: %s; } p { margin-top: 0; }", family, size));
return kit;
return new HTMLEditorKit() {
@Override
public StyleSheet getStyleSheet() {
return style;
}
};
}
public static void removeScrollBorder(final Component c) {