changeset 52861 | e93d73b51fd0 |
parent 52849 | 199e9fa5a5c2 |
child 52862 | 930ce8eacb87 |
--- 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 }