src/Pure/PIDE/command.scala
changeset 69647 70f1994988d4
parent 68758 a110e7e24e55
child 70068 b9985133805d
     1.1 --- a/src/Pure/PIDE/command.scala	Fri Jan 11 16:36:21 2019 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Fri Jan 11 22:34:28 2019 +0100
     1.3 @@ -79,6 +79,7 @@
     1.4  
     1.5    final class Exports private(private val rep: SortedMap[Long, Export.Entry])
     1.6    {
     1.7 +    def is_empty: Boolean = rep.isEmpty
     1.8      def iterator: Iterator[Exports.Entry] = rep.iterator
     1.9  
    1.10      def + (entry: Exports.Entry): Exports =