--- a/src/Tools/jEdit/src/jedit_lib.scala Fri Nov 15 16:08:56 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Fri Nov 15 16:50:44 2024 +0100
@@ -295,7 +295,7 @@
}
- /* graphics range */
+ /* font */
def init_font_context(view: View, painter: TextAreaPainter): Unit = {
painter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
@@ -311,6 +311,9 @@
font = painter.getFont,
context = painter.getFontRenderContext)
+
+ /* graphics range */
+
case class Gfx_Range(x: Int, y: Int, length: Int)
// NB: jEdit always normalizes \r\n and \r to \n