# HG changeset patch
# User wenzelm
# Date 1393509074 -3600
# Node ID 3086f57e48e9a6a353105dde3fa435e33d9dd957
# Parent  9b243afbbe8393ebb4a22c282198017796172973
reparse only for actually changed blobs;
tuned signature;

diff -r 9b243afbbe83 -r 3086f57e48e9 src/Pure/PIDE/command.scala
--- 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
 
diff -r 9b243afbbe83 -r 3086f57e48e9 src/Pure/Thy/thy_syntax.scala
--- 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
 
diff -r 9b243afbbe83 -r 3086f57e48e9 src/Tools/jEdit/src/document_model.scala
--- 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,