src/Pure/General/long_name.scala
author wenzelm
Mon Apr 03 14:29:44 2017 +0200 (2017-04-03)
changeset 65358 e345e9420109
parent 56800 b904ea8edd73
child 65440 fd147f56d9be
permissions -rw-r--r--
proper qualifier (again, see df4cd6e1fdfa);
     1 /*  Title:      Pure/General/long_name.scala
     2     Author:     Makarius
     3 
     4 Long names.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Long_Name
    11 {
    12   val separator = "."
    13   val separator_char = '.'
    14 
    15   def is_qualified(name: String): Boolean = name.contains(separator_char)
    16 
    17   def implode(names: List[String]): String = names.mkString(separator)
    18   def explode(name: String): List[String] = Library.space_explode(separator_char, name)
    19 
    20   def qualify(qual: String, name: String): String =
    21     if (qual == "" || name == "") name
    22     else qual + separator + name
    23 
    24   def base_name(name: String): String =
    25     if (name == "") ""
    26     else explode(name).last
    27 }