# HG changeset patch
# User wenzelm
# Date 1608732110 -3600
# Node ID a8050df4f58f6385bd4e421028bf85e514853da9
# Parent  adda33fdb5d04f8f334b13f5e28a67990e96cbc5
clarified fonts, notably for Windows L&F;

diff -r adda33fdb5d0 -r a8050df4f58f Admin/components/components.sha1
--- a/Admin/components/components.sha1	Tue Dec 22 23:59:45 2020 +0100
+++ b/Admin/components/components.sha1	Wed Dec 23 15:01:50 2020 +0100
@@ -183,6 +183,7 @@
 b9c6f49d3f6ebe2e85a50595ce7412d01a4314ac  jedit_build-20190717.tar.gz
 1c753beb93e92e95e99e8ead23a68346bd1af44a  jedit_build-20200610.tar.gz
 533b1ee6459f59bcbe4f09e214ad2cb990fb6952  jedit_build-20200908.tar.gz
+f9966b5ed26740bb5b8bddbfe947fcefaea43d4d  jedit_build-20201223.tar.gz
 0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa  jfreechart-1.0.14-1.tar.gz
 8122526f1fc362ddae1a328bdbc2152853186fee  jfreechart-1.0.14.tar.gz
 d911f63a5c9b4c7335bb73f805cb1711ce017a84  jfreechart-1.5.0.tar.gz
diff -r adda33fdb5d0 -r a8050df4f58f Admin/components/main
--- a/Admin/components/main	Tue Dec 22 23:59:45 2020 +0100
+++ b/Admin/components/main	Wed Dec 23 15:01:50 2020 +0100
@@ -6,7 +6,7 @@
 e-2.5-1
 isabelle_fonts-20190717
 jdk-11.0.9+11
-jedit_build-20200908
+jedit_build-20201223
 jfreechart-1.5.1
 jortho-1.0-2
 kodkodi-1.5.6
diff -r adda33fdb5d0 -r a8050df4f58f src/Tools/jEdit/patches/panel_font
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/panel_font	Wed Dec 23 15:01:50 2020 +0100
@@ -0,0 +1,28 @@
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/gui/PanelWindowContainer.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/gui/PanelWindowContainer.java	2020-09-03 05:31:02.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java	2020-12-23 13:16:31.059779643 +0100
+@@ -52,6 +52,7 @@
+ import javax.swing.JComponent;
+ import javax.swing.JPanel;
+ import javax.swing.JPopupMenu;
++import javax.swing.JMenuItem;
+ import javax.swing.JToggleButton;
+ import javax.swing.UIManager;
+ import javax.swing.border.Border;
+@@ -163,6 +164,7 @@
+ 		{
+ 			button = new JToggleButton();	
+ 			button.setMargin(new Insets(1,1,1,1));
++            button.setFont(new JMenuItem().getFont());
+ 		}
+ 		GenericGUIUtilities.setButtonContentMargin(button, new Insets(6,6,6,6));
+ 		button.setRequestFocusEnabled(false);
+@@ -690,8 +692,6 @@
+ 			renderHints = new RenderingHints(
+ 				RenderingHints.KEY_ANTIALIASING,
+ 				RenderingHints.VALUE_ANTIALIAS_ON);
+-			renderHints.put(RenderingHints.KEY_FRACTIONALMETRICS,
+-				RenderingHints.VALUE_FRACTIONALMETRICS_ON);
+ 			renderHints.put(RenderingHints.KEY_RENDERING,
+ 				RenderingHints.VALUE_RENDER_QUALITY);
+ 		} //}}}