src/Tools/jEdit/src/document_model.scala

   }
 
   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()
 
     if (Isabelle.continuous_checking && is_theory) {
       val snapshot = this.snapshot()

           if !JEdit_Lib.jedit_text_areas(blob_buffer).isEmpty
           start <- snapshot.node.command_start(cmd)
           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))
-    }
-    else empty_perspective
+      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 (false, empty_perspective)
   }
 
 
   /* blob */
 

   {
     Swing_Thread.require()
 
     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),
         node_name -> Document.Node.Clear(),
         node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),

   {
     private var pending_clear = false
     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
         node_edits(clear, edits, perspective)
       }

       pending += e
       PIDE.editor.invoke()
     }
   }
 
+  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 */
 
   private val buffer_listener: BufferListener = new BufferAdapter