# HG changeset patch
# User wenzelm
# Date 1333814135 -7200
# Node ID d760049b2d189797fab1959185f58807976713cf
# Parent  6a08fd7a607171253098afd0f71d5d08e0b9b1f4
more robust update_perspective, e.g. required after reload of buffer that is not at start position;

diff -r 6a08fd7a6071 -r d760049b2d18 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Sat Apr 07 17:49:20 2012 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Sat Apr 07 17:55:35 2012 +0200
@@ -95,7 +95,6 @@
   private object pending_edits  // owned by Swing thread
   {
     private val pending = new mutable.ListBuffer[Text.Edit]
-    private var pending_perspective = false
     private var last_perspective: Text.Perspective = Text.Perspective.empty
 
     def snapshot(): List[Text.Edit] = pending.toList
@@ -104,16 +103,12 @@
     {
       Swing_Thread.require()
 
-      val new_perspective =
-        if (pending_perspective) { pending_perspective = false; perspective() }
-        else last_perspective
-
-      snapshot() match {
-        case Nil if last_perspective == new_perspective =>
-        case edits =>
-          pending.clear
-          last_perspective = new_perspective
-          session.edit_node(name, node_header(), new_perspective, edits)
+      val edits = snapshot()
+      val new_perspective = perspective()
+      if (!edits.isEmpty || last_perspective != new_perspective) {
+        pending.clear
+        last_perspective = new_perspective
+        session.edit_node(name, node_header(), new_perspective, edits)
       }
     }
 
@@ -129,7 +124,6 @@
 
     def update_perspective()
     {
-      pending_perspective = true
       delay_flush(true)
     }