--- 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)