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 =