1.1 --- a/src/Tools/jEdit/src/document_model.scala	Sat Apr 07 17:49:20 2012 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sat Apr 07 17:55:35 2012 +0200
     1.3 @@ -95,7 +95,6 @@
     1.4    private object pending_edits  // owned by Swing thread
     1.5    {
     1.6      private val pending = new mutable.ListBuffer[Text.Edit]
     1.7 -    private var pending_perspective = false
     1.8      private var last_perspective: Text.Perspective = Text.Perspective.empty
     1.9  
    1.10      def snapshot(): List[Text.Edit] = pending.toList
    1.11 @@ -104,16 +103,12 @@
    1.12      {
    1.13        Swing_Thread.require()
    1.14  
    1.15 -      val new_perspective =
    1.16 -        if (pending_perspective) { pending_perspective = false; perspective() }
    1.17 -        else last_perspective
    1.18 -
    1.19 -      snapshot() match {
    1.20 -        case Nil if last_perspective == new_perspective =>
    1.21 -        case edits =>
    1.22 -          pending.clear
    1.23 -          last_perspective = new_perspective
    1.24 -          session.edit_node(name, node_header(), new_perspective, edits)
    1.25 +      val edits = snapshot()
    1.26 +      val new_perspective = perspective()
    1.27 +      if (!edits.isEmpty || last_perspective != new_perspective) {
    1.28 +        pending.clear
    1.29 +        last_perspective = new_perspective
    1.30 +        session.edit_node(name, node_header(), new_perspective, edits)
    1.31        }
    1.32      }
    1.33  
    1.34 @@ -129,7 +124,6 @@
    1.35  
    1.36      def update_perspective()
    1.37      {
    1.38 -      pending_perspective = true
    1.39        delay_flush(true)
    1.40      }
    1.41