# HG changeset patch
# User wenzelm
# Date 1265404062 -3600
# Node ID b89a31957950be9ef83d013faa366d8a3664d24d
# Parent  e0d01e77c7b1dbc7b6914710ff444c68dcc1b236
filter out identical completions only after symbols.decode -- recover completion of literal symbols (e.g. \<AA>);

diff -r e0d01e77c7b1 -r b89a31957950 src/Pure/Thy/completion.scala
--- 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(_ < _))
             }
diff -r e0d01e77c7b1 -r b89a31957950 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- 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]]) { }
     }
   }
-
 }