author | wenzelm |
Wed, 22 Jun 2011 16:32:36 +0200 | |
changeset 43506 | bf7400573617 |
parent 43504 | 4ffb4ca04fb8 |
permissions | -rw-r--r-- |
43506 | 1 |
diff -ru 4.4.1/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 4.4.1/jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java |
2 |
--- 4.4.1/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2011-06-21 01:28:56.000000000 +0200 |
|
3 |
+++ 4.4.1/jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2011-06-22 16:18:43.000000000 +0200 |
|
43504
4ffb4ca04fb8
avoid fractional font metrics, which makes rendering really ugly (e.g. on Linux);
wenzelm
parents:
diff
changeset
|
4 |
@@ -646,7 +646,7 @@ |
4ffb4ca04fb8
avoid fractional font metrics, which makes rendering really ugly (e.g. on Linux);
wenzelm
parents:
diff
changeset
|
5 |
this.font = font; |
4ffb4ca04fb8
avoid fractional font metrics, which makes rendering really ugly (e.g. on Linux);
wenzelm
parents:
diff
changeset
|
6 |
|
4ffb4ca04fb8
avoid fractional font metrics, which makes rendering really ugly (e.g. on Linux);
wenzelm
parents:
diff
changeset
|
7 |
FontRenderContext fontRenderContext |
4ffb4ca04fb8
avoid fractional font metrics, which makes rendering really ugly (e.g. on Linux);
wenzelm
parents:
diff
changeset
|
8 |
- = new FontRenderContext(null,true,true); |
4ffb4ca04fb8
avoid fractional font metrics, which makes rendering really ugly (e.g. on Linux);
wenzelm
parents:
diff
changeset
|
9 |
+ = new FontRenderContext(null,true,false); |
4ffb4ca04fb8
avoid fractional font metrics, which makes rendering really ugly (e.g. on Linux);
wenzelm
parents:
diff
changeset
|
10 |
glyphs = font.createGlyphVector(fontRenderContext,text); |
4ffb4ca04fb8
avoid fractional font metrics, which makes rendering really ugly (e.g. on Linux);
wenzelm
parents:
diff
changeset
|
11 |
width = (int)glyphs.getLogicalBounds().getWidth() + 4; |
4ffb4ca04fb8
avoid fractional font metrics, which makes rendering really ugly (e.g. on Linux);
wenzelm
parents:
diff
changeset
|
12 |
//height = (int)glyphs.getLogicalBounds().getHeight(); |
43506 | 13 |