# HG changeset patch
# User wenzelm
# Date 1489523787 -3600
# Node ID e955b33f432c7be270e01d610842e16662ef8f59
# Parent  1f53b94701168907cffc284c22282599305af43d
proper plugin access;

diff -r 1f53b9470116 -r e955b33f432c src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Tue Mar 14 21:32:12 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Mar 14 21:36:27 2017 +0100
@@ -243,7 +243,7 @@
           else Nil
 
         val st1 = st.copy(models = st.models ++ file_edits.map(_._2) -- purge_edits.map(_._1))
-        PIDE.file_watcher.purge(
+        PIDE.plugin.file_watcher.purge(
           (for {
             (_, model) <- st1.file_models_iterator
             file <- model.file
@@ -311,7 +311,7 @@
     pending_edits: List[Text.Edit] = Nil): File_Model =
   {
     val file = PIDE.resources.node_name_file(node_name)
-    file.foreach(PIDE.file_watcher.register_parent(_))
+    file.foreach(PIDE.plugin.file_watcher.register_parent(_))
 
     val content = Document_Model.File_Content(text)
     File_Model(session, node_name, file, content, node_required, last_perspective, pending_edits)
diff -r 1f53b9470116 -r e955b33f432c src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Mar 14 21:32:12 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Mar 14 21:36:27 2017 +0100
@@ -43,9 +43,6 @@
 
   def debugger: Debugger = session.debugger
 
-  def file_watcher(): File_Watcher =
-    if (plugin == null) File_Watcher.none else plugin.file_watcher
-
   lazy val editor = new JEdit_Editor
 
 
@@ -424,6 +421,6 @@
 
     exit_models(JEdit_Lib.jedit_buffers().toList)
     PIDE.session.stop()
-    PIDE.file_watcher.shutdown()
+    file_watcher.shutdown()
   }
 }