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