reparse only for actually changed blobs;
tuned signature;

--- a/src/Pure/PIDE/command.scala	Thu Feb 27 14:15:23 2014 +0100
+++ b/src/Pure/PIDE/command.scala	Thu Feb 27 14:51:14 2014 +0100
@@ -340,6 +340,9 @@
 
   /* blobs */
 
+  def blobs_changed(doc_blobs: Document.Blobs): Boolean =
+    blobs.exists({ case Exn.Res((name, _)) => doc_blobs.changed(name) case _ => false })
+
   def blobs_names: List[Document.Node.Name] =
     for (Exn.Res((name, _)) <- blobs) yield name
 

--- a/src/Pure/Thy/thy_syntax.scala	Thu Feb 27 14:15:23 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Feb 27 14:51:14 2014 +0100
@@ -448,8 +448,9 @@
       val reparse =
         (reparse0 /: nodes0.entries)({
           case (reparse, (name, node)) =>
-            if (node.thy_load_commands.isEmpty) reparse
-            else name :: reparse
+            if (node.thy_load_commands.exists(_.blobs_changed(doc_blobs)))
+              name :: reparse
+            else reparse
           })
       val reparse_set = reparse.toSet
 

--- a/src/Tools/jEdit/src/document_model.scala	Thu Feb 27 14:15:23 2014 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Feb 27 14:51:14 2014 +0100
@@ -125,8 +125,7 @@
           range = snapshot.convert(cmd.proper_range + start)
         } yield range
 
-      val reparse =
-        snapshot.node.thy_load_commands.exists(cmd => cmd.blobs_names.exists(doc_blobs.changed))
+      val reparse = snapshot.node.thy_load_commands.exists(_.blobs_changed(doc_blobs))
 
       (reparse,
         Document.Node.Perspective(node_required,