tuned signature --- avoid confusion with init_view(buffer: Buffer, text_area: JEditTextArea);
--- 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()