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);
authorwenzelm
Mon, 01 Feb 2021 18:12:44 +0100
changeset 73223 ee2e803fcf57
parent 73222 e18191f2aed9
child 73224 49686e3b1909
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);
Admin/components/components.sha1
Admin/components/main
src/Tools/jEdit/patches/laf_fonts
--- a/Admin/components/components.sha1	Mon Feb 01 17:15:00 2021 +0100
+++ b/Admin/components/components.sha1	Mon Feb 01 18:12:44 2021 +0100
@@ -192,6 +192,7 @@
 1c753beb93e92e95e99e8ead23a68346bd1af44a  jedit_build-20200610.tar.gz
 533b1ee6459f59bcbe4f09e214ad2cb990fb6952  jedit_build-20200908.tar.gz
 f9966b5ed26740bb5b8bddbfe947fcefaea43d4d  jedit_build-20201223.tar.gz
+0bdbd36eda5992396e9c6b66aa24259d4dd7559c  jedit_build-20210201.tar.gz
 0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa  jfreechart-1.0.14-1.tar.gz
 8122526f1fc362ddae1a328bdbc2152853186fee  jfreechart-1.0.14.tar.gz
 d911f63a5c9b4c7335bb73f805cb1711ce017a84  jfreechart-1.5.0.tar.gz
--- a/Admin/components/main	Mon Feb 01 17:15:00 2021 +0100
+++ b/Admin/components/main	Mon Feb 01 18:12:44 2021 +0100
@@ -7,7 +7,7 @@
 flatlaf-1.0-rc2
 isabelle_fonts-20190717
 jdk-15.0.2+7
-jedit_build-20201223
+jedit_build-20210201
 jfreechart-1.5.1
 jortho-1.0-2
 kodkodi-1.5.6
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/laf_fonts	Mon Feb 01 18:12:44 2021 +0100
@@ -0,0 +1,13 @@
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/options/AppearanceOptionPane.java	2020-09-03 05:31:04.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/options/AppearanceOptionPane.java	2021-02-01 18:00:07.541681144 +0100
+@@ -414,7 +414,9 @@
+ 
+ 		// adjust swing properties for button, menu, and label, and list and
+ 		// textfield fonts
+-		setFonts();
++		if (!jEdit.getProperty("lookAndFeel").startsWith("com.formdev.flatlaf.")) {
++			setFonts();
++		}
+ 
+ 		// This is handled a little differently from other jEdit settings
+ 		// as this flag needs to be known very early in the