src/Pure/General/completion.scala
changeset 56599 c4424d8c890f
parent 56591 1a59587f46ec
child 56600 628e039cc34d
--- a/src/Pure/General/completion.scala	Tue Apr 15 22:41:10 2014 +0200
+++ b/src/Pure/General/completion.scala	Wed Apr 16 09:38:40 2014 +0200
@@ -173,7 +173,7 @@
           if xname1 != original
           (full_name, descr_name) =
             if (kind == "") (name, quote(decode(name)))
-            else (kind + "." + name, Library.plain_words(kind) + " " + quote(decode(name)))
+            else (kind + "." + name, Word.plain_words(kind) + " " + quote(decode(name)))
           description = List(xname1, "(" + descr_name + ")")
         } yield Item(range, original, full_name, description, xname1, 0, true)