| author | wenzelm |
| Sat, 01 Dec 2018 15:55:04 +0100 | |
| changeset 69382 | d70767e508d7 |
| child 69838 | 4419d4d675c3 |
| permissions | -rw-r--r-- |
|
69382
d70767e508d7
proper menu accelerator font for Java 11 (no update of jedit-build component yet);
wenzelm
parents:
diff
changeset
|
1 |
diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java |
|
d70767e508d7
proper menu accelerator font for Java 11 (no update of jedit-build component yet);
wenzelm
parents:
diff
changeset
|
2 |
--- 5.5.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2018-12-01 15:51:30.320182833 +0100 |
|
d70767e508d7
proper menu accelerator font for Java 11 (no update of jedit-build component yet);
wenzelm
parents:
diff
changeset
|
3 |
+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java 2018-12-01 15:51:49.028286932 +0100 |
|
d70767e508d7
proper menu accelerator font for Java 11 (no update of jedit-build component yet);
wenzelm
parents:
diff
changeset
|
4 |
@@ -1172,7 +1172,7 @@ |
|
d70767e508d7
proper menu accelerator font for Java 11 (no update of jedit-build component yet);
wenzelm
parents:
diff
changeset
|
5 |
return new Font("Monospaced", Font.PLAIN, 12);
|
|
d70767e508d7
proper menu accelerator font for Java 11 (no update of jedit-build component yet);
wenzelm
parents:
diff
changeset
|
6 |
} |
|
d70767e508d7
proper menu accelerator font for Java 11 (no update of jedit-build component yet);
wenzelm
parents:
diff
changeset
|
7 |
else {
|
|
d70767e508d7
proper menu accelerator font for Java 11 (no update of jedit-build component yet);
wenzelm
parents:
diff
changeset
|
8 |
- Font font2 = new Font("Lucida Sans Typewriter", Font.PLAIN, font1.getSize());
|
|
d70767e508d7
proper menu accelerator font for Java 11 (no update of jedit-build component yet);
wenzelm
parents:
diff
changeset
|
9 |
+ Font font2 = new Font("Isabelle DejaVu Sans Mono", Font.PLAIN, font1.getSize());
|
|
d70767e508d7
proper menu accelerator font for Java 11 (no update of jedit-build component yet);
wenzelm
parents:
diff
changeset
|
10 |
FontRenderContext frc = new FontRenderContext(null, true, false); |
|
d70767e508d7
proper menu accelerator font for Java 11 (no update of jedit-build component yet);
wenzelm
parents:
diff
changeset
|
11 |
float scale = |
|
d70767e508d7
proper menu accelerator font for Java 11 (no update of jedit-build component yet);
wenzelm
parents:
diff
changeset
|
12 |
font1.getLineMetrics("", frc).getHeight() / font2.getLineMetrics("", frc).getHeight();
|