Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/jEdit/patches/laf_fonts
author wenzelm
Sun, 17 Nov 2024 13:57:50 +0100
changeset 81474 a3dc66165d15
parent 81297 07f64697408e
child 82654 60bd591ef3fc
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
81297
07f64697408e update to jedit5.7.0;
wenzelm
parents: 73223
diff changeset 
     1
 
diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java
07f64697408e update to jedit5.7.0;
wenzelm
parents: 73223
diff changeset 
     2
 
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java	2024-08-03 19:53:15.000000000 +0200
07f64697408e update to jedit5.7.0;
wenzelm
parents: 73223
diff changeset 
     3
 
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java	2024-10-29 11:50:54.062016616 +0100
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 
     4
 
@@ -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 
     5
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
 
 		// 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 
     7
 
 		// 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 
     8
 
-		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 
     9
 
+		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 
    10
 
+			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 
    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
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
 
 		// 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 
    14
 
 		// as this flag needs to be known very early in the
81297
07f64697408e update to jedit5.7.0;
wenzelm
parents: 73223
diff changeset 
    15
 
diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/View.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/View.java
isabelle