more detailed description of completion items;

--- a/src/Pure/General/completion.ML	Fri Mar 07 13:29:10 2014 +0100
+++ b/src/Pure/General/completion.ML	Fri Mar 07 14:37:25 2014 +0100
@@ -7,7 +7,7 @@
 signature COMPLETION =
 sig
   type T
-  val names: Position.T -> (string * string) list -> T
+  val names: Position.T -> (string * (string * string)) list -> T
   val none: T
   val reported_text: T -> string
   val report: T -> unit
@@ -17,7 +17,8 @@
 structure Completion: COMPLETION =
 struct
 
-abstype T = Completion of {pos: Position.T, total: int, names: (string * string) list}
+abstype T =
+  Completion of {pos: Position.T, total: int, names: (string * (string * string)) list}
 with
 
 (* completion of names *)
@@ -40,7 +41,7 @@
       let
         val markup = Position.markup pos Markup.completion;
         val body = (total, names) |>
-          let open XML.Encode in pair int (list (pair string string)) end;
+          let open XML.Encode in pair int (list (pair string (pair string string))) end;
       in YXML.string_of (XML.Elem (markup, body)) end
     else ""
   end;

--- a/src/Pure/General/completion.scala	Fri Mar 07 13:29:10 2014 +0100
+++ b/src/Pure/General/completion.scala	Fri Mar 07 14:37:25 2014 +0100
@@ -136,7 +136,7 @@
               val (total, names) =
               {
                 import XML.Decode._
-                pair(int, list(pair(string, string)))(body)
+                pair(int, list(pair(string, pair(string, string))))(body)
               }
               Some(Names(info.range, total, names))
             }
@@ -148,21 +148,27 @@
     }
   }
 
-  sealed case class Names(range: Text.Range, total: Int, names: List[(String, String)])
+  sealed case class Names(
+    range: Text.Range, total: Int, names: List[(String, (String, String))])
   {
     def no_completion: Boolean = total == 0 && names.isEmpty
 
     def complete(
       history: Completion.History,
-      decode: Boolean,
+      do_decode: Boolean,
       original: String): Option[Completion.Result] =
     {
+      def decode(s: String): String = if (do_decode) Symbol.decode(s) else s
       val items =
         for {
-          (xname, name) <- names
-          xname1 = (if (decode) Symbol.decode(xname) else xname)
+          (xname, (kind, name)) <- names
+          xname1 = decode(xname)
           if xname1 != original
-        } yield Item(range, original, name, xname1, xname1, 0, true)
+          (full_name, descr_name) =
+            if (kind == "") (name, quote(decode(name)))
+            else (kind + "." + name, Library.plain_words(kind) + " " + quote(decode(name)))
+          description = xname1 + "   (" + descr_name + ")"
+        } yield Item(range, original, full_name, description, xname1, 0, true)
 
       if (items.isEmpty) None
       else Some(Result(range, original, names.length == 1, items.sorted(history.ordering)))
@@ -298,7 +304,7 @@
 
   def complete(
     history: Completion.History,
-    decode: Boolean,
+    do_decode: Boolean,
     explicit: Boolean,
     start: Text.Offset,
     text: CharSequence,
@@ -306,6 +312,7 @@
     extend_word: Boolean,
     language_context: Completion.Language_Context): Option[Completion.Result] =
   {
+    def decode(s: String): String = if (do_decode) Symbol.decode(s) else s
     val length = text.length
 
     val abbrevs_result =
@@ -356,21 +363,28 @@
     words_result match {
       case Some(((word, cs), end)) =>
         val range = Text.Range(- word.length, 0) + end + start
-        val ds = (if (decode) cs.map(Symbol.decode(_)) else cs).filter(_ != word)
+        val ds = cs.map(decode(_)).filter(_ != word)
         if (ds.isEmpty) None
         else {
           val immediate =
             !Completion.Word_Parsers.is_word(word) &&
             Character.codePointCount(word, 0, word.length) > 1
           val items =
-            ds.map(s => {
+            for { (name, name1) <- cs zip ds }
+            yield {
               val (s1, s2) =
-                space_explode(Completion.caret_indicator, s) match {
+                space_explode(Completion.caret_indicator, name1) match {
                   case List(s1, s2) => (s1, s2)
-                  case _ => (s, "")
+                  case _ => (name1, "")
                 }
-              Completion.Item(range, word, s, s, s1 + s2, - s2.length, explicit || immediate)
-            })
+              val description =
+                if (keywords(name)) name1 + "   (keyword)"
+                else if (Symbol.names.isDefinedAt(name) && name != name1)
+                  name1 + "   (symbol " + quote(name) + ")"
+                else name1
+              Completion.Item(
+                range, word, name1, description, s1 + s2, - s2.length, explicit || immediate)
+            }
           Some(Completion.Result(range, word, cs.length == 1, items.sorted(history.ordering)))
         }
       case None => None

--- a/src/Pure/General/name_space.ML	Fri Mar 07 13:29:10 2014 +0100
+++ b/src/Pure/General/name_space.ML	Fri Mar 07 14:37:25 2014 +0100
@@ -214,7 +214,7 @@
         Symtab.fold
           (fn (a, (name :: _, _)) =>
               if String.isPrefix x a andalso not (is_concealed space name)
-              then cons (ext name, Long_Name.implode [kind, name]) else I
+              then cons (ext name, (kind, name)) else I
             | _ => I) internals []
         |> sort_distinct (string_ord o pairself #1);
     in Completion.names pos names end

--- a/src/Pure/library.scala	Fri Mar 07 13:29:10 2014 +0100
+++ b/src/Pure/library.scala	Fri Mar 07 14:37:25 2014 +0100
@@ -97,6 +97,9 @@
     else ""
   }
 
+  def plain_words(str: String): String =
+    space_explode('_', str).mkString(" ")
+
 
   /* strings */
 

--- a/src/Tools/jEdit/src/rendering.scala	Fri Mar 07 13:29:10 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Fri Mar 07 14:37:25 2014 +0100
@@ -459,7 +459,7 @@
           case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
             Some(Text.Info(r, (t1 + t2, info)))
           case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
-            val kind1 = space_explode('_', kind).mkString(" ")
+            val kind1 = Library.plain_words(kind)
             val txt1 = kind1 + " " + quote(name)
             val t = prev.info._1
             val txt2 =