| 56800 |      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 | }
 | 
|  |     28 | 
 |