diff -r f155c38242c1 -r e93d73b51fd0 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Aug 05 11:08:54 2013 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Aug 05 15:03:52 2013 +0200
@@ -28,7 +28,9 @@
   {
     def + (o: Overlay) = new Overlays(rep + o)
     def - (o: Overlay) = new Overlays(rep - o)
+    def is_empty: Boolean = rep.isEmpty
     def dest: List[Overlay] = rep.toList
+    def commands: Set[Command] = rep.iterator.map(x => x._1).toSet
   }