tuned signature --- avoid confusion with init_view(buffer: Buffer, text_area: JEditTextArea);
authorwenzelm
Tue, 07 Apr 2020 20:36:09 +0200
changeset 71724 522994a6c10e
parent 71723 5bbd80875e02
child 71725 c255ed582095
tuned signature --- avoid confusion with init_view(buffer: Buffer, text_area: JEditTextArea);
src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Apr 07 17:03:57 2020 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Apr 07 20:36:09 2020 +0200
@@ -289,7 +289,7 @@
   @volatile private var startup_failure: Option[Throwable] = None
   @volatile private var startup_notified = false
 
-  private def init_view(view: View)
+  private def init_editor(view: View)
   {
     Session_Build.check_dialog(view)
     Keymap_Merge.check_dialog(view)
@@ -341,7 +341,7 @@
           jEdit.propertiesChanged()
 
           val view = jEdit.getActiveView()
-          init_view(view)
+          init_editor(view)
 
           PIDE.editor.hyperlink_position(true, Document.Snapshot.init,
             JEdit_Sessions.logic_root(options.value)).foreach(_.follow(view))
@@ -480,7 +480,7 @@
     shutting_down.change(_ => false)
 
     val view = jEdit.getActiveView()
-    if (view != null) init_view(view)
+    if (view != null) init_editor(view)
   }
 
   override def stop()