propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
tuned signature;

--- a/src/Pure/PIDE/resources.scala	Sat Mar 29 10:17:09 2014 +0100
+++ b/src/Pure/PIDE/resources.scala	Sat Mar 29 10:49:32 2014 +0100
@@ -91,15 +91,15 @@
     with_thy_text(name, check_thy_text(name, _))
 
 
-  /* theory text edits */
+  /* document changes */
 
-  def parse_edits(
+  def parse_change(
       reparse_limit: Int,
       previous: Document.Version,
       doc_blobs: Document.Blobs,
       edits: List[Document.Edit_Text]): Session.Change =
-    Thy_Syntax.parse_edits(this, reparse_limit, previous, doc_blobs, edits)
+    Thy_Syntax.parse_change(this, reparse_limit, previous, doc_blobs, edits)
 
-  def syntax_changed() { }
+  def commit(change: Session.Change) { }
 }
 

--- a/src/Pure/PIDE/session.scala	Sat Mar 29 10:17:09 2014 +0100
+++ b/src/Pure/PIDE/session.scala	Sat Mar 29 10:49:32 2014 +0100
@@ -24,6 +24,7 @@
     previous: Document.Version,
     doc_blobs: Document.Blobs,
     syntax_changed: Boolean,
+    deps_changed: Boolean,
     doc_edits: List[Document.Edit_Command],
     version: Document.Version)
 
@@ -190,8 +191,8 @@
         case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
           val prev = previous.get_finished
           val change =
-            Timing.timeit("parse_edits", timing) {
-              resources.parse_edits(reparse_limit, prev, doc_blobs, text_edits)
+            Timing.timeit("parse_change", timing) {
+              resources.parse_change(reparse_limit, prev, doc_blobs, text_edits)
             }
           version_result.fulfill(change.version)
           sender ! change
@@ -402,8 +403,7 @@
       val assignment = global_state().the_assignment(change.previous).check_finished
       global_state >> (_.define_version(change.version, assignment))
       prover.get.update(change.previous.id, change.version.id, change.doc_edits)
-
-      if (change.syntax_changed) resources.syntax_changed()
+      resources.commit(change)
     }
     //}}}
 

--- a/src/Pure/Thy/thy_syntax.scala	Sat Mar 29 10:17:09 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Sat Mar 29 10:49:32 2014 +0100
@@ -156,7 +156,8 @@
     base_syntax: Outer_Syntax,
     previous: Document.Version,
     edits: List[Document.Edit_Text]):
-    ((Outer_Syntax, Boolean), List[Document.Node.Name], Document.Nodes, List[Document.Edit_Command]) =
+    (Outer_Syntax, Boolean, Boolean, List[Document.Node.Name], Document.Nodes,
+      List[Document.Edit_Command]) =
   {
     var updated_imports = false
     var updated_keywords = false
@@ -178,7 +179,7 @@
       case _ =>
     }
 
-    val syntax =
+    val (syntax, syntax_changed) =
       if (previous.is_init || updated_keywords) {
         val syntax =
           (base_syntax /: nodes.entries) {
@@ -193,7 +194,7 @@
         nodes.descendants(doc_edits.iterator.map(_._1).toList)
       else Nil
 
-    (syntax, reparse, nodes, doc_edits.toList)
+    (syntax, syntax_changed, updated_imports, reparse, nodes, doc_edits.toList)
   }
 
 
@@ -431,62 +432,59 @@
     }
   }
 
-  def parse_edits(
+  def parse_change(
       resources: Resources,
       reparse_limit: Int,
       previous: Document.Version,
       doc_blobs: Document.Blobs,
       edits: List[Document.Edit_Text]): Session.Change =
   {
-    val ((syntax, syntax_changed), reparse0, nodes0, doc_edits0) =
+    val (syntax, syntax_changed, deps_changed, reparse0, nodes0, doc_edits0) =
       header_edits(resources.base_syntax, previous, edits)
 
-    if (edits.isEmpty)
-      Session.Change(previous, doc_blobs, false, Nil, Document.Version.make(syntax, previous.nodes))
-    else {
-      val reparse =
-        (reparse0 /: nodes0.entries)({
-          case (reparse, (name, node)) =>
-            if (node.load_commands.exists(_.blobs_changed(doc_blobs)))
-              name :: reparse
-            else reparse
-          })
-      val reparse_set = reparse.toSet
+    val (doc_edits, version) =
+      if (edits.isEmpty) (Nil, Document.Version.make(syntax, previous.nodes))
+      else {
+        val reparse =
+          (reparse0 /: nodes0.entries)({
+            case (reparse, (name, node)) =>
+              if (node.load_commands.exists(_.blobs_changed(doc_blobs)))
+                name :: reparse
+              else reparse
+            })
+        val reparse_set = reparse.toSet
 
-      var nodes = nodes0
-      val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0
+        var nodes = nodes0
+        val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0
 
-      val node_edits =
-        (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
-          .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]]  // FIXME ???
+        val node_edits =
+          (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
+            .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]]  // FIXME ???
 
-      node_edits foreach {
-        case (name, edits) =>
-          val node = nodes(name)
-          val commands = node.commands
+        node_edits foreach {
+          case (name, edits) =>
+            val node = nodes(name)
+            val commands = node.commands
 
-          val node1 =
-            if (reparse_set(name) && !commands.isEmpty)
-              node.update_commands(
-                reparse_spans(resources, syntax, doc_blobs,
-                  name, commands, commands.head, commands.last))
-            else node
-          val node2 = (node1 /: edits)(text_edit(resources, syntax, doc_blobs, reparse_limit, _, _))
+            val node1 =
+              if (reparse_set(name) && !commands.isEmpty)
+                node.update_commands(
+                  reparse_spans(resources, syntax, doc_blobs,
+                    name, commands, commands.head, commands.last))
+              else node
+            val node2 =
+              (node1 /: edits)(text_edit(resources, syntax, doc_blobs, reparse_limit, _, _))
 
-          if (!(node.same_perspective(node2.perspective)))
-            doc_edits += (name -> node2.perspective)
+            if (!(node.same_perspective(node2.perspective)))
+              doc_edits += (name -> node2.perspective)
 
-          doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
+            doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
 
-          nodes += (name -> node2)
+            nodes += (name -> node2)
+        }
+        (doc_edits.toList, Document.Version.make(syntax, nodes))
       }
 
-      Session.Change(
-        previous,
-        doc_blobs,
-        syntax_changed,
-        doc_edits.toList,
-        Document.Version.make(syntax, nodes))
-    }
+    Session.Change(previous, doc_blobs, syntax_changed, deps_changed, doc_edits, version)
   }
 }

--- a/src/Tools/jEdit/src/jedit_resources.scala	Sat Mar 29 10:17:09 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Sat Mar 29 10:49:32 2014 +0100
@@ -117,7 +117,10 @@
 
   /* theory text edits */
 
-  override def syntax_changed(): Unit =
-    Swing_Thread.later { jEdit.propertiesChanged() }
+  override def commit(change: Session.Change)
+  {
+    if (change.syntax_changed) Swing_Thread.later { jEdit.propertiesChanged() }
+    if (change.deps_changed) PIDE.deps_changed()
+  }
 }
 

--- a/src/Tools/jEdit/src/plugin.scala	Sat Mar 29 10:17:09 2014 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Sat Mar 29 10:49:32 2014 +0100
@@ -39,6 +39,7 @@
   @volatile var session: Session = new Session(new JEdit_Resources(Set.empty, Outer_Syntax.empty))
 
   def options_changed() { plugin.options_changed() }
+  def deps_changed() { plugin.deps_changed() }
 
   def resources(): JEdit_Resources =
     session.resources.asInstanceOf[JEdit_Resources]
@@ -168,13 +169,19 @@
 
 class Plugin extends EBPlugin
 {
-  /* options */
+  /* global changes */
 
-  def options_changed() {
+  def options_changed()
+  {
     PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
     Swing_Thread.later { delay_load.invoke() }
   }
 
+  def deps_changed()
+  {
+    Swing_Thread.later { delay_load.invoke() }
+  }
+
 
   /* theory files */