| author | wenzelm |
| Sun, 21 Aug 2022 12:35:45 +0200 | |
| changeset 75944 | abc3e052ba5d |
| parent 73223 | ee2e803fcf57 |
| child 81297 | 07f64697408e |
| permissions | -rw-r--r-- |
|
73223
ee2e803fcf57
avoid interference with FlatLaf fonts, see also jEdit SVN 24885 'Updated Appearance option pane to allow setting "primary" and "secondary" fonts for all look and feels.' (daleanson 2018-08-30);
wenzelm
parents:
diff
changeset
|
1 |
--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/options/AppearanceOptionPane.java 2020-09-03 05:31:04.000000000 +0200 |
|
ee2e803fcf57
avoid interference with FlatLaf fonts, see also jEdit SVN 24885 'Updated Appearance option pane to allow setting "primary" and "secondary" fonts for all look and feels.' (daleanson 2018-08-30);
wenzelm
parents:
diff
changeset
|
2 |
+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/options/AppearanceOptionPane.java 2021-02-01 18:00:07.541681144 +0100 |
|
ee2e803fcf57
avoid interference with FlatLaf fonts, see also jEdit SVN 24885 'Updated Appearance option pane to allow setting "primary" and "secondary" fonts for all look and feels.' (daleanson 2018-08-30);
wenzelm
parents:
diff
changeset
|
3 |
@@ -414,7 +414,9 @@ |
|
ee2e803fcf57
avoid interference with FlatLaf fonts, see also jEdit SVN 24885 'Updated Appearance option pane to allow setting "primary" and "secondary" fonts for all look and feels.' (daleanson 2018-08-30);
wenzelm
parents:
diff
changeset
|
4 |
|
|
ee2e803fcf57
avoid interference with FlatLaf fonts, see also jEdit SVN 24885 'Updated Appearance option pane to allow setting "primary" and "secondary" fonts for all look and feels.' (daleanson 2018-08-30);
wenzelm
parents:
diff
changeset
|
5 |
// adjust swing properties for button, menu, and label, and list and |
|
ee2e803fcf57
avoid interference with FlatLaf fonts, see also jEdit SVN 24885 'Updated Appearance option pane to allow setting "primary" and "secondary" fonts for all look and feels.' (daleanson 2018-08-30);
wenzelm
parents:
diff
changeset
|
6 |
// textfield fonts |
|
ee2e803fcf57
avoid interference with FlatLaf fonts, see also jEdit SVN 24885 'Updated Appearance option pane to allow setting "primary" and "secondary" fonts for all look and feels.' (daleanson 2018-08-30);
wenzelm
parents:
diff
changeset
|
7 |
- setFonts(); |
|
ee2e803fcf57
avoid interference with FlatLaf fonts, see also jEdit SVN 24885 'Updated Appearance option pane to allow setting "primary" and "secondary" fonts for all look and feels.' (daleanson 2018-08-30);
wenzelm
parents:
diff
changeset
|
8 |
+ if (!jEdit.getProperty("lookAndFeel").startsWith("com.formdev.flatlaf.")) {
|
|
ee2e803fcf57
avoid interference with FlatLaf fonts, see also jEdit SVN 24885 'Updated Appearance option pane to allow setting "primary" and "secondary" fonts for all look and feels.' (daleanson 2018-08-30);
wenzelm
parents:
diff
changeset
|
9 |
+ setFonts(); |
|
ee2e803fcf57
avoid interference with FlatLaf fonts, see also jEdit SVN 24885 'Updated Appearance option pane to allow setting "primary" and "secondary" fonts for all look and feels.' (daleanson 2018-08-30);
wenzelm
parents:
diff
changeset
|
10 |
+ } |
|
ee2e803fcf57
avoid interference with FlatLaf fonts, see also jEdit SVN 24885 'Updated Appearance option pane to allow setting "primary" and "secondary" fonts for all look and feels.' (daleanson 2018-08-30);
wenzelm
parents:
diff
changeset
|
11 |
|
|
ee2e803fcf57
avoid interference with FlatLaf fonts, see also jEdit SVN 24885 'Updated Appearance option pane to allow setting "primary" and "secondary" fonts for all look and feels.' (daleanson 2018-08-30);
wenzelm
parents:
diff
changeset
|
12 |
// This is handled a little differently from other jEdit settings |
|
ee2e803fcf57
avoid interference with FlatLaf fonts, see also jEdit SVN 24885 'Updated Appearance option pane to allow setting "primary" and "secondary" fonts for all look and feels.' (daleanson 2018-08-30);
wenzelm
parents:
diff
changeset
|
13 |
// as this flag needs to be known very early in the |