src/Pure/PIDE/document.scala
changeset 57621 caa37976801f
parent 57620 c30ab960875e
child 57842 8e4ae2db1849
--- 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]