# HG changeset patch
# User wenzelm
# Date 1586284569 -7200
# Node ID 522994a6c10e494a7277e18161670f3f04501a1e
# Parent  5bbd80875e02d84357cbb263b7f34c6a6a8e3c1d
tuned signature --- avoid confusion with init_view(buffer: Buffer, text_area: JEditTextArea);

diff -r 5bbd80875e02 -r 522994a6c10e 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()