# HG changeset patch
# User wenzelm
# Date 1398856284 -7200
# Node ID b904ea8edd73c079d729ca9952982c79f90c382a
# Parent  00b13fb87b3a7e6b225c57a66d4ad32de9aff62c
support for long names in Scala;

diff -r 00b13fb87b3a -r b904ea8edd73 src/Pure/General/completion.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)
diff -r 00b13fb87b3a -r b904ea8edd73 src/Pure/General/long_name.ML
--- 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;
diff -r 00b13fb87b3a -r b904ea8edd73 src/Pure/General/long_name.scala
--- /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
+}
+
diff -r 00b13fb87b3a -r b904ea8edd73 src/Pure/build-jars
--- 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