--- 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)
}