proper update of text perspective for nodes with changed blobs, which is important to refresh the corresponding command perspective (otherwise it might refer to invalid thy_load commands and cause full execution of the node by the prover);

--- a/src/Tools/jEdit/src/document_model.scala	Thu Feb 27 10:59:12 2014 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Feb 27 12:37:43 2014 +0100
@@ -99,7 +99,8 @@
   val empty_perspective: Document.Node.Perspective_Text =
     Document.Node.Perspective(false, Text.Perspective.empty, Document.Node.Overlays.empty)
 
-  def node_perspective(): Document.Node.Perspective_Text =
+  def node_perspective(changed_blobs: Set[Document.Node.Name])
+    : (Boolean, Document.Node.Perspective_Text) =
   {
     Swing_Thread.require()
 
@@ -125,11 +126,15 @@
           range = snapshot.convert(cmd.proper_range + start)
         } yield range
 
-      Document.Node.Perspective(node_required,
-        Text.Perspective(document_view_ranges ::: thy_load_ranges),
-        PIDE.editor.node_overlays(node_name))
+      val reparse =
+        snapshot.node.thy_load_commands.exists(cmd => cmd.blobs_names.exists(changed_blobs(_)))
+
+      (reparse,
+        Document.Node.Perspective(node_required,
+          Text.Perspective(document_view_ranges ::: thy_load_ranges),
+          PIDE.editor.node_overlays(node_name)))
     }
-    else empty_perspective
+    else (false, empty_perspective)
   }
 
 
@@ -160,7 +165,7 @@
 
     val header = node_header()
     val text = JEdit_Lib.buffer_text(buffer)
-    val perspective = node_perspective()
+    val (_, perspective) = node_perspective(Set.empty)
 
     if (is_theory)
       List(session.header_edit(node_name, header),
@@ -205,14 +210,15 @@
     private val pending = new mutable.ListBuffer[Text.Edit]
     private var last_perspective = empty_perspective
 
+    def is_pending(): Boolean = pending_clear || !pending.isEmpty
     def snapshot(): List[Text.Edit] = pending.toList
 
-    def flushed_edits(): List[Document.Edit_Text] =
+    def flushed_edits(changed_blobs: Set[Document.Node.Name]): List[Document.Edit_Text] =
     {
       val clear = pending_clear
       val edits = snapshot()
-      val perspective = node_perspective()
-      if (clear || !edits.isEmpty || last_perspective != perspective) {
+      val (reparse, perspective) = node_perspective(changed_blobs)
+      if (clear || reparse || !edits.isEmpty || last_perspective != perspective) {
         pending_clear = false
         pending.clear
         last_perspective = perspective
@@ -234,11 +240,14 @@
     }
   }
 
+  def has_pending_edits(): Boolean =
+    Swing_Thread.require { pending_edits.is_pending() }
+
   def snapshot(): Document.Snapshot =
     Swing_Thread.require { session.snapshot(node_name, pending_edits.snapshot()) }
 
-  def flushed_edits(): List[Document.Edit_Text] =
-    Swing_Thread.require { pending_edits.flushed_edits() }
+  def flushed_edits(changed_blobs: Set[Document.Node.Name]): List[Document.Edit_Text] =
+    Swing_Thread.require { pending_edits.flushed_edits(changed_blobs) }
 
 
   /* buffer listener */

--- a/src/Tools/jEdit/src/jedit_editor.scala	Thu Feb 27 10:59:12 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Thu Feb 27 12:37:43 2014 +0100
@@ -26,7 +26,16 @@
   {
     Swing_Thread.require()
 
-    val edits = PIDE.document_models().flatMap(_.flushed_edits())
+    val models = PIDE.document_models()
+    val changed_blobs =
+      (for {
+        model <- models.iterator
+        if !model.is_theory && model.has_pending_edits
+      } yield model.node_name).toSet
+
+    System.console.writer.println("\nchanged_blobs = " + changed_blobs)
+
+    val edits = models.flatMap(_.flushed_edits(changed_blobs))
     if (!edits.isEmpty) session.update(PIDE.document_blobs(), edits)
   }