# HG changeset patch
# User wenzelm
# Date 1731682901 -3600
# Node ID 0c29878ae48fdc9f891da050cbf139830d17ce09
# Parent  d92d754b5dd906941d56856ab26dde252ff3e8dc
more accurate initial FontRenderContext, notably on macOS, Windows, or Linux with "env GDK_SCALE=2";

diff -r d92d754b5dd9 -r 0c29878ae48f src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Fri Nov 15 15:18:48 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri Nov 15 16:01:41 2024 +0100
@@ -12,6 +12,7 @@
 import java.io.{File => JFile}
 import java.awt.{Component, Container, GraphicsEnvironment, Point, Rectangle, Dimension, Toolkit}
 import java.awt.event.{InputEvent, KeyEvent, KeyListener}
+import java.awt.font.FontRenderContext
 import javax.swing.{Icon, ImageIcon, JScrollBar, JWindow, SwingUtilities}
 
 import scala.util.parsing.input.CharSequenceReader
@@ -22,7 +23,7 @@
 import org.gjt.sp.jedit.io.{FileVFS, VFSManager}
 import org.gjt.sp.jedit.gui.{KeyEventWorkaround, KeyEventTranslator}
 import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager}
-import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter, Selection}
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter, Selection, AntiAlias}
 
 
 object JEdit_Lib {
@@ -296,6 +297,15 @@
 
   /* graphics range */
 
+  def init_font_context(view: View, painter: TextAreaPainter): Unit = {
+    painter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
+    painter.setFractionalFontMetricsEnabled(jEdit.getBooleanProperty("view.fracFontMetrics"))
+    val old = painter.getFontRenderContext
+    Untyped.set[FontRenderContext](painter, "fontRenderContext",
+      new FontRenderContext(view.getGraphicsConfiguration.getDefaultTransform,
+        old.getAntiAliasingHint, old.getFractionalMetricsHint))
+  }
+
   def font_metric(painter: TextAreaPainter): Font_Metric =
     new Font_Metric(
       font = painter.getFont,
diff -r d92d754b5dd9 -r 0c29878ae48f src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Fri Nov 15 15:18:48 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Fri Nov 15 16:01:41 2024 +0100
@@ -21,7 +21,7 @@
 
 import org.gjt.sp.jedit.{jEdit, View, Registers, JEditBeanShellAction}
 import org.gjt.sp.jedit.input.{DefaultInputHandlerProvider, TextAreaInputHandler}
-import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea}
+import org.gjt.sp.jedit.textarea.JEditEmbeddedTextArea
 import org.gjt.sp.jedit.syntax.SyntaxStyle
 import org.gjt.sp.jedit.gui.KeyEventTranslator
 import org.gjt.sp.util.{SyntaxUtilities, Log}
@@ -63,10 +63,8 @@
   def refresh(): Unit = {
     GUI_Thread.require {}
 
-    val font = current_font_info.font
-    getPainter.setFont(font)
-    getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
-    getPainter.setFractionalFontMetricsEnabled(jEdit.getBooleanProperty("view.fracFontMetrics"))
+    getPainter.setFont(current_font_info.font)
+    JEdit_Lib.init_font_context(view, getPainter)
     getPainter.setStyles(
       SyntaxUtilities.loadStyles(current_font_info.family, current_font_info.size.round))
     getPainter.setLineExtraSpacing(jEdit.getIntegerProperty("options.textarea.lineSpacing", 0))