src/Pure/General/long_name.scala

--- a/src/Pure/General/long_name.scala	Sat Apr 08 12:31:29 2017 +0200
+++ b/src/Pure/General/long_name.scala	Sat Apr 08 12:47:34 2017 +0200
@@ -21,6 +21,10 @@
     if (qual == "" || name == "") name
     else qual + separator + name
 
+  def qualifier(name: String): String =
+    if (name == "") ""
+    else implode(explode(name).dropRight(1))
+
   def base_name(name: String): String =
     if (name == "") ""
     else explode(name).last