src/Pure/General/long_name.scala

clarified signature;

/*  Title:      Pure/General/long_name.scala
    Author:     Makarius

Long names.
*/

package isabelle


object Long_Name {
  val separator = "."
  val separator_char = '.'

  def is_qualified(name: String): Boolean = name.contains(separator_char)

  def implode(names: List[String]): String = names.mkString(separator)
  def explode(name: String): List[String] = space_explode(separator_char, name)

  def qualify(qual: String, name: String): String =
    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

  def try_unqualify(qual: String, name: String): Option[String] = {
    val m = qual.length
    val n = name.length
    if (0 < m && m < n && name.startsWith(qual) && name(m) == separator_char)
      Some(name.substring(m + 1))
    else None
  }
}