# HG changeset patch
# User wenzelm
# Date 1731070554 -3600
# Node ID 874e12fb6c3d9a55b380cd5b0ecae5c6ab557db9
# Parent  4a62c57fe7459bb446de878056024400f23f72af
tuned: fewer warnings in IntelliJ IDEA;

diff -r 4a62c57fe745 -r 874e12fb6c3d src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Fri Nov 08 13:42:25 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri Nov 08 13:55:54 2024 +0100
@@ -46,7 +46,7 @@
     val old_content = dummy_window.getContentPane
 
     dummy_window.setContentPane(outer)
-    dummy_window.pack
+    dummy_window.pack()
     dummy_window.revalidate()
 
     val geometry =
@@ -252,17 +252,20 @@
       try {
         val p = text_area.offsetToXY(range.start)
         val (q, r) =
-          if (get_text(buffer, Text.Range(stop - 1, stop)) == Some("\n"))
+          if (get_text(buffer, Text.Range(stop - 1, stop)).contains("\n")) {
             (text_area.offsetToXY(stop - 1), char_width)
-          else if (stop >= end)
+          }
+          else if (stop >= end) {
             (text_area.offsetToXY(end), char_width * (stop - end))
+          }
           else (text_area.offsetToXY(stop), 0)
         (p, q, r)
       }
       catch { case _: ArrayIndexOutOfBoundsException => (null, null, 0) }
 
-    if (p != null && q != null && p.x < q.x + r && p.y == q.y)
+    if (p != null && q != null && p.x < q.x + r && p.y == q.y) {
       Some(Gfx_Range(p.x, p.y, q.x + r - p.x))
+    }
     else None
   }