filter out identical completions only after symbols.decode -- recover completion of literal symbols (e.g. \<AA>);

--- a/src/Pure/Thy/completion.scala	Fri Feb 05 20:19:40 2010 +0100
+++ b/src/Pure/Thy/completion.scala	Fri Feb 05 22:07:42 2010 +0100
@@ -88,12 +88,11 @@
     abbrevs_lex.parse(abbrevs_lex.keyword, new Library.Reverse(line)) match {
       case abbrevs_lex.Success(rev_a, _) =>
         val (word, c) = abbrevs_map(rev_a)
-        if (word == c) None
-        else Some(word, List(c))
+        Some(word, List(c))
       case _ =>
         Completion.Parse.read(line) match {
           case Some(word) =>
-            words_lex.completions(word).map(words_map(_)).filter(_ != word) match {
+            words_lex.completions(word).map(words_map(_)) match {
               case Nil => None
               case cs => Some(word, cs.sort(_ < _))
             }

--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Fri Feb 05 20:19:40 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Fri Feb 05 22:07:42 2010 +0100
@@ -88,11 +88,11 @@
       case None => null
       case Some((word, cs)) =>
         val ds =
-          if (Isabelle_Encoding.is_active(buffer))
+          (if (Isabelle_Encoding.is_active(buffer))
             cs.map(Isabelle.system.symbols.decode(_)).sort(_ < _)
-          else cs
-        new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
+           else cs).filter(_ != word)
+        if (ds.isEmpty) null
+        else new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
     }
   }
-
 }