src/Tools/jEdit/src/document_model.scala

--- a/src/Tools/jEdit/src/document_model.scala	Tue Aug 23 21:19:24 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Aug 24 13:03:39 2011 +0200
@@ -87,15 +87,17 @@
   private object pending_edits  // owned by Swing thread
   {
     private val pending = new mutable.ListBuffer[Text.Edit]
+    private var pending_perspective = false
     def snapshot(): List[Text.Edit] = pending.toList
 
     def flush()
     {
       Swing_Thread.require()
       snapshot() match {
-        case Nil =>
+        case Nil if !pending_perspective =>
         case edits =>
           pending.clear
+          pending_perspective = false
           session.edit_node(node_name, master_dir, node_header(), perspective(), edits)
       }
     }
@@ -116,6 +118,18 @@
       pending += edit
       delay_flush()
     }
+
+    def update_perspective()
+    {
+      pending_perspective = true
+      delay_flush()
+    }
+  }
+
+  def update_perspective()
+  {
+    Swing_Thread.require()
+    pending_edits.update_perspective()
   }