support for long names in Scala;

--- a/src/Pure/General/completion.scala	Wed Apr 30 12:12:44 2014 +0200
+++ b/src/Pure/General/completion.scala	Wed Apr 30 13:11:24 2014 +0200
@@ -174,7 +174,7 @@
           (full_name, descr_name) =
             if (kind == "") (name, quote(decode(name)))
             else
-             (kind + "." + name,
+             (Long_Name.qualify(kind, name),
               Word.implode(Word.explode('_', kind)) + " " + quote(decode(name)))
           description = List(xname1, "(" + descr_name + ")")
         } yield Item(range, original, full_name, description, xname1, 0, true)

--- a/src/Pure/General/long_name.ML	Wed Apr 30 12:12:44 2014 +0200
+++ b/src/Pure/General/long_name.ML	Wed Apr 30 13:11:24 2014 +0200
@@ -26,6 +26,7 @@
 struct
 
 val separator = ".";
+
 val is_qualified = exists_string (fn s => s = separator);
 
 fun hidden name = "??." ^ name;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/long_name.scala	Wed Apr 30 13:11:24 2014 +0200
@@ -0,0 +1,28 @@
+/*  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] = Library.space_explode(separator_char, name)
+
+  def qualify(qual: String, name: String): String =
+    if (qual == "" || name == "") name
+    else qual + separator + name
+
+  def base_name(name: String): String =
+    if (name == "") ""
+    else explode(name).last
+}
+

--- a/src/Pure/build-jars	Wed Apr 30 12:12:44 2014 +0200
+++ b/src/Pure/build-jars	Wed Apr 30 13:11:24 2014 +0200
@@ -24,6 +24,7 @@
   General/graph.scala
   General/graphics_file.scala
   General/linear_set.scala
+  General/long_name.scala
   General/multi_map.scala
   General/output.scala
   General/path.scala