--- 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 =