early filtering of unchanged perspective;

--- a/src/Tools/jEdit/src/document_model.scala	Wed Aug 24 13:37:43 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Aug 24 13:38:07 2011 +0200
@@ -88,17 +88,24 @@
   {
     private val pending = new mutable.ListBuffer[Text.Edit]
     private var pending_perspective = false
+    private var last_perspective: Text.Perspective = Nil
+
     def snapshot(): List[Text.Edit] = pending.toList
 
     def flush()
     {
       Swing_Thread.require()
+
+      val new_perspective =
+        if (pending_perspective) { pending_perspective = false; perspective() }
+        else last_perspective
+
       snapshot() match {
-        case Nil if !pending_perspective =>
+        case Nil if new_perspective == last_perspective =>
         case edits =>
           pending.clear
-          pending_perspective = false
-          session.edit_node(node_name, master_dir, node_header(), perspective(), edits)
+          last_perspective = new_perspective
+          session.edit_node(node_name, master_dir, node_header(), new_perspective, edits)
       }
     }