| author | wenzelm |
| Wed, 10 Jun 2020 19:59:12 +0200 | |
| changeset 71932 | 65fd0f032a75 |
| parent 69838 | 4419d4d675c3 |
| child 72247 | c06260b7152c |
| permissions | -rw-r--r-- |
|
71932
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
69838
diff
changeset
|
1 |
diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/GUIUtilities.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java |
|
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
69838
diff
changeset
|
2 |
--- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/GUIUtilities.java 2020-05-20 11:10:13.000000000 +0200 |
|
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
69838
diff
changeset
|
3 |
+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java 2020-06-10 15:30:42.744707440 +0200 |
|
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
69838
diff
changeset
|
4 |
@@ -1130,9 +1130,7 @@ |
|
69382
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 {
|
|
71932
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
69838
diff
changeset
|
8 |
- Font font2 = |
|
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
69838
diff
changeset
|
9 |
- new Font(OperatingSystem.isWindows() ? "Lucida Console" : "Monospaced", |
|
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
69838
diff
changeset
|
10 |
- Font.PLAIN, font1.getSize()); |
|
69382
d70767e508d7
proper menu accelerator font for Java 11 (no update of jedit-build component yet);
wenzelm
parents:
diff
changeset
|
11 |
+ 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
|
12 |
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
|
13 |
float scale = |
|
d70767e508d7
proper menu accelerator font for Java 11 (no update of jedit-build component yet);
wenzelm
parents:
diff
changeset
|
14 |
font1.getLineMetrics("", frc).getHeight() / font2.getLineMetrics("", frc).getHeight();
|