# HG changeset patch
# User wenzelm
# Date 1314185887 -7200
# Node ID 0fc38897248a46103079b2f493467e8f63550b65
# Parent  bebe1579919270e283fedc0cdf8b27b8e45476e3
early filtering of unchanged perspective;

diff -r bebe15799192 -r 0fc38897248a src/Tools/jEdit/src/document_model.scala
--- 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)
       }
     }