# HG changeset patch
# User wenzelm
# Date 1742914241 -3600
# Node ID 6e80327eb30ac0d211014e0f0dbae888c1e01e88
# Parent  a01c1f8743622d9b61c29afbe0fffd09866f1b10
tuned: fewer warnings in IntelliJ IDEA;

diff -r a01c1f874362 -r 6e80327eb30a src/Tools/jEdit/src/font_info.scala
--- a/src/Tools/jEdit/src/font_info.scala	Tue Mar 25 13:53:07 2025 +0100
+++ b/src/Tools/jEdit/src/font_info.scala	Tue Mar 25 15:50:41 2025 +0100
@@ -49,7 +49,7 @@
         jEdit.setIntegerProperty("view.fontsize", size)
         jEdit.propertiesChanged()
         jEdit.saveSettings()
-        jEdit.getActiveView().getStatus.setMessageAndClear("Text font size: " + size)
+        jEdit.getActiveView.getStatus.setMessageAndClear("Text font size: " + size)
       }
     }
 
diff -r a01c1f874362 -r 6e80327eb30a src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Tue Mar 25 13:53:07 2025 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Tue Mar 25 15:50:41 2025 +0100
@@ -111,7 +111,7 @@
     jEdit.getViewManager().getViews().asScala.iterator
 
   def jedit_view(view: View = null): View =
-    if (view == null) jEdit.getActiveView() else view
+    if (view == null) jEdit.getActiveView else view
 
   def jedit_edit_panes(view: View): Iterator[EditPane] =
     if (view == null) Iterator.empty
@@ -406,7 +406,7 @@
   /* key event handling */
 
   def request_focus_view(alt_view: View = null): Unit = {
-    val view = if (alt_view != null) alt_view else jEdit.getActiveView()
+    val view = if (alt_view != null) alt_view else jEdit.getActiveView
     if (view != null) {
       val text_area = view.getTextArea
       if (text_area != null) text_area.requestFocus()
diff -r a01c1f874362 -r 6e80327eb30a src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Tue Mar 25 13:53:07 2025 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala	Tue Mar 25 15:50:41 2025 +0100
@@ -311,7 +311,7 @@
 
           jEdit.propertiesChanged()
 
-          val view = jEdit.getActiveView()
+          val view = jEdit.getActiveView
           init_editor(view)
 
           PIDE.editor.hyperlink_position(true, Document.Snapshot.init,
@@ -446,7 +446,7 @@
 
     shutting_down.change(_ => false)
 
-    val view = jEdit.getActiveView()
+    val view = jEdit.getActiveView
     if (view != null) init_editor(view)
   }