update File_Model based on file-system events;

--- a/src/Pure/General/file_watcher.scala	Mon Jan 09 21:51:39 2017 +0100
+++ b/src/Pure/General/file_watcher.scala	Mon Jan 09 22:54:48 2017 +0100
@@ -25,9 +25,10 @@
 
 object File_Watcher
 {
+  val none: File_Watcher = new File_Watcher
+
   def apply(handle: Set[JFile] => Unit, delay: => Time = Time.seconds(0.5)): File_Watcher =
-    if (Platform.is_windows) new File_Watcher
-    else new Impl(handle, delay)
+    if (Platform.is_windows) none else new Impl(handle, delay)
 
 
   /* proper implementation */

--- a/src/Tools/jEdit/src/document_model.scala	Mon Jan 09 21:51:39 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Jan 09 22:54:48 2017 +0100
@@ -11,6 +11,8 @@
 
 import isabelle._
 
+import java.io.{File => JFile}
+
 import scala.collection.mutable
 
 import org.gjt.sp.jedit.{jEdit, View}
@@ -70,6 +72,7 @@
       else {
         val edit = Text.Edit.insert(0, text)
         val model = File_Model(session, node_name, File_Content(text), pending_edits = List(edit))
+        model.watch
         copy(models = models + (node_name -> model))
       }
   }
@@ -87,6 +90,31 @@
     } yield Text.Info(range, (entry, model))
 
 
+  /* sync external files */
+
+  def sync_files(changed_files: Set[JFile]): Boolean =
+  {
+    state.change_result(st =>
+      {
+        val changed_models =
+          (for {
+            model <- st.file_models_iterator
+            node_name = model.node_name
+            file <- PIDE.resources.node_name_file(node_name)
+            if changed_files(file)
+            text <- PIDE.resources.read_file_content(node_name)
+            if model.content.text != text
+          } yield {
+            val content = Document_Model.File_Content(text)
+            val edits = Text.Edit.replace(0, model.content.text, text)
+            (node_name, model.copy(content = content, pending_edits = model.pending_edits ::: edits))
+          }).toList
+        if (changed_models.isEmpty) (false, st)
+        else (true, st.copy(models = (st.models /: changed_models)(_ + _)))
+      })
+  }
+
+
   /* syntax */
 
   def syntax_changed(names: List[Document.Node.Name])
@@ -313,6 +341,13 @@
 
   def is_stable: Boolean = pending_edits.isEmpty
   def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
+
+
+  /* watch file-system content */
+
+  def watch: Unit =
+    for (file <- PIDE.resources.node_name_file(node_name))
+      PIDE.file_watcher.register_parent(file)
 }
 
 case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer)
@@ -522,7 +557,10 @@
     init_token_marker()
 
     val content = Document_Model.File_Content(JEdit_Lib.buffer_text(buffer))
-    File_Model(session, node_name, content, node_required,
-      pending_edits.get_last_perspective, pending_edits.get_edits)
+    val model =
+      File_Model(session, node_name, content, node_required,
+        pending_edits.get_last_perspective, pending_edits.get_edits)
+    model.watch
+    model
   }
 }

--- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Jan 09 21:51:39 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Jan 09 22:54:48 2017 +0100
@@ -47,6 +47,12 @@
     Document.Node.Name(node, master_dir, theory)
   }
 
+  def node_name_file(name: Document.Node.Name): Option[JFile] =
+  {
+    val vfs = VFSManager.getVFSForPath(name.node)
+    if (vfs.isInstanceOf[FileVFS]) Some(new JFile(name.node)) else None
+  }
+
   def theory_node_name(buffer: Buffer): Option[Document.Node.Name] =
   {
     val name = node_name(buffer)

--- a/src/Tools/jEdit/src/plugin.scala	Mon Jan 09 21:51:39 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Jan 09 22:54:48 2017 +0100
@@ -11,6 +11,8 @@
 
 import javax.swing.JOptionPane
 
+import java.io.{File => JFile}
+
 import scala.swing.{ListView, ScrollPane}
 
 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug, PerspectiveManager}
@@ -43,6 +45,9 @@
   def resources(): JEdit_Resources =
     session.resources.asInstanceOf[JEdit_Resources]
 
+  def file_watcher(): File_Watcher =
+    if (plugin == null) File_Watcher.none else plugin.file_watcher
+
   lazy val editor = new JEdit_Editor
 
 
@@ -233,6 +238,12 @@
   private lazy val delay_load =
     GUI_Thread.delay_last(PIDE.options.seconds("editor_load_delay")) { delay_load_action() }
 
+  private def file_watcher_action(changed: Set[JFile]): Unit =
+    if (Document_Model.sync_files(changed)) PIDE.editor.invoke_generated()
+
+  lazy val file_watcher: File_Watcher =
+    File_Watcher(file_watcher_action _, PIDE.options.seconds("editor_load_delay"))
+
 
   /* session phase */
 
@@ -419,5 +430,6 @@
     PIDE.session.phase_changed -= session_phase
     PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
     PIDE.session.stop()
+    PIDE.file_watcher.shutdown()
   }
 }