# HG changeset patch
# User wenzelm
# Date 1731944891 -3600
# Node ID f02d3e52a7d5c5c2d17f65c24222c8f02e8419df
# Parent  7d4df25af57271580033552c80edbec2eff2e44f
tuned output: formatting is pointless for proportional font;

diff -r 7d4df25af572 -r f02d3e52a7d5 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Mon Nov 18 15:05:31 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Mon Nov 18 16:48:11 2024 +0100
@@ -37,7 +37,7 @@
   ) {
     lazy val match_ranges: List[Text.Range] = JEdit_Lib.search_text(buffer, line_range, regex)
     lazy val line_text: String = JEdit_Lib.get_text(buffer, line_range).get
-    lazy val gui_text: String = "% 3d".format(line) + ": " + Library.trim_line(line_text)
+    lazy val gui_text: String = line.toString + ": " + Library.trim_line(line_text)
     override def toString: String = gui_text
   }