tuned: fewer warnings in IntelliJ IDEA;
authorwenzelm
Tue, 25 Mar 2025 15:50:41 +0100
changeset 82403 6e80327eb30a
parent 82402 a01c1f874362
child 82404 47c4ea946fc8
tuned: fewer warnings in IntelliJ IDEA;
src/Tools/jEdit/src/font_info.scala
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/main_plugin.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)
       }
     }
 
--- 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()
--- 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)
   }