# HG changeset patch
# User wenzelm
# Date 1731685844 -3600
# Node ID b99b531f13e67081d1c32bcc1bc1a4ac47274bc0
# Parent  b3a90bff348ae76b6a1854c8754730e0f6b1bf1f
tuned comments;

diff -r b3a90bff348a -r b99b531f13e6 src/Tools/jEdit/src/jedit_lib.scala
--- 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