# HG changeset patch
# User wenzelm
# Date 1406127363 -7200
# Node ID caa37976801f35d5c9ae1d597999de504a1bd99b
# Parent  c30ab960875e6cbdecf718a8d9b83a548f2f3be3
more frugal edits;

diff -r c30ab960875e -r caa37976801f src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Jul 23 16:20:07 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Jul 23 16:56:03 2014 +0200
@@ -156,6 +156,12 @@
           case _ =>
         }
       }
+
+      def is_void: Boolean =
+        this match {
+          case Edits(Nil) => true
+          case _ => false
+        }
     }
     case class Clear[A, B]() extends Edit[A, B]
     case class Blob[A, B](blob: Document.Blob) extends Edit[A, B]
diff -r c30ab960875e -r caa37976801f src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Jul 23 16:20:07 2014 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Jul 23 16:56:03 2014 +0200
@@ -164,22 +164,26 @@
       clear: Boolean,
       text_edits: List[Text.Edit],
       perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] =
-    get_blob() match {
-      case None =>
-        val header_edit = session.header_edit(node_name, node_header())
-        if (clear)
-          List(header_edit,
-            node_name -> Document.Node.Clear(),
-            node_name -> Document.Node.Edits(text_edits),
-            node_name -> perspective)
-        else
-          List(header_edit,
-            node_name -> Document.Node.Edits(text_edits),
-            node_name -> perspective)
-      case Some(blob) =>
-        List(node_name -> Document.Node.Blob(blob),
-          node_name -> Document.Node.Edits(text_edits))
-    }
+  {
+    val edits: List[Document.Edit_Text] =
+      get_blob() match {
+        case None =>
+          val header_edit = session.header_edit(node_name, node_header())
+          if (clear)
+            List(header_edit,
+              node_name -> Document.Node.Clear(),
+              node_name -> Document.Node.Edits(text_edits),
+              node_name -> perspective)
+          else
+            List(header_edit,
+              node_name -> Document.Node.Edits(text_edits),
+              node_name -> perspective)
+        case Some(blob) =>
+          List(node_name -> Document.Node.Blob(blob),
+            node_name -> Document.Node.Edits(text_edits))
+      }
+    edits.filterNot(_._2.is_void)
+  }
 
 
   /* pending edits */