src/Pure/PIDE/command.scala

--- a/src/Pure/PIDE/command.scala	Fri Jan 11 16:36:21 2019 +0100
+++ b/src/Pure/PIDE/command.scala	Fri Jan 11 22:34:28 2019 +0100
@@ -79,6 +79,7 @@
 
   final class Exports private(private val rep: SortedMap[Long, Export.Entry])
   {
+    def is_empty: Boolean = rep.isEmpty
     def iterator: Iterator[Exports.Entry] = rep.iterator
 
     def + (entry: Exports.Entry): Exports =