# HG changeset patch
# User wenzelm
# Date 1547242468 -3600
# Node ID 70f1994988d4a6cf4b911e45b416d321f738f438
# Parent  3d91a7a581130f589b43a14cf71b8669b2782a00
more operations;

diff -r 3d91a7a58113 -r 70f1994988d4 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 =
diff -r 3d91a7a58113 -r 70f1994988d4 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Fri Jan 11 16:36:21 2019 +0100
+++ b/src/Pure/Thy/export.scala	Fri Jan 11 22:34:28 2019 +0100
@@ -13,6 +13,15 @@
 
 object Export
 {
+  /* structured name */
+
+  val sep_char: Char = '/'
+  val sep: String = sep_char.toString
+
+  def explode_name(s: String): List[String] = space_explode(sep_char, s)
+  def implode_name(elems: Iterable[String]): String = elems.mkString(sep)
+
+
   /* SQL data model */
 
   object Data
@@ -75,6 +84,11 @@
   {
     override def toString: String = uncompressed().toString
 
+    val name_elems: List[String] = explode_name(name)
+
+    def name_extends(elems: List[String]): Boolean =
+      name_elems.startsWith(elems) && name_elems != elems
+
     def text: String = uncompressed().text
 
     def uncompressed(cache: XZ.Cache = XZ.cache()): Bytes =