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]