# HG changeset patch
# User wenzelm
# Date 1377861854 -7200
# Node ID ffabc0083786a6376bd3f79980775be48a73fb37
# Parent  c12a3edcd8e4c98b086ab98a93dd95bfa1607bc8
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);

diff -r c12a3edcd8e4 -r ffabc0083786 src/Pure/Isar/completion.scala
--- a/src/Pure/Isar/completion.scala	Fri Aug 30 12:59:28 2013 +0200
+++ b/src/Pure/Isar/completion.scala	Fri Aug 30 13:24:14 2013 +0200
@@ -11,7 +11,7 @@
 
 object Completion
 {
-  /* items */
+  /* result */
 
   sealed case class Item(
     original: String,
@@ -20,6 +20,8 @@
     immediate: Boolean)
   { override def toString: String = description }
 
+  sealed case class Result(original: String, unique: Boolean, items: List[Item])
+
 
   /* init */
 
@@ -92,8 +94,7 @@
 
   /* complete */
 
-  def complete(decode: Boolean, explicit: Boolean, line: CharSequence)
-    : Option[(String, List[Completion.Item])] =
+  def complete(decode: Boolean, explicit: Boolean, line: CharSequence): Option[Completion.Result] =
   {
     val raw_result =
       abbrevs_lex.parse(abbrevs_lex.keyword, new Library.Reverse(line)) match {
@@ -115,13 +116,14 @@
       }
     raw_result match {
       case Some((word, cs)) =>
-        val ds = (if (decode) cs.map(Symbol.decode(_)).sorted else cs)
+        val ds = (if (decode) cs.map(Symbol.decode(_)).sorted else cs).filter(_ != word)
         if (ds.isEmpty) None
         else {
           val immediate =
             !Completion.is_word(word) &&
             Character.codePointCount(word, 0, word.length) > 1
-          Some((word, ds.map(s => Completion.Item(word, s, s, explicit || immediate))))
+          val items = ds.map(s => Completion.Item(word, s, s, explicit || immediate))
+          Some(Completion.Result(word, cs.length == 1, items))
         }
       case None => None
     }
diff -r c12a3edcd8e4 -r ffabc0083786 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Fri Aug 30 12:59:28 2013 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Fri Aug 30 13:24:14 2013 +0200
@@ -108,30 +108,31 @@
 
             val decode = Isabelle_Encoding.is_active(buffer)
             syntax.completion.complete(decode, explicit, text) match {
-              case Some((_, List(item))) if item.immediate && immediate =>
-                insert(item)
+              case Some(result) =>
+                if (result.unique && result.items.head.immediate && immediate)
+                  insert(result.items.head)
+                else {
+                  val font =
+                    painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
 
-              case Some((original, items)) =>
-                val font =
-                  painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
+                  val loc1 = text_area.offsetToXY(caret - result.original.length)
+                  if (loc1 != null) {
+                    val loc2 =
+                      SwingUtilities.convertPoint(painter,
+                        loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
 
-                val loc1 = text_area.offsetToXY(caret - original.length)
-                if (loc1 != null) {
-                  val loc2 =
-                    SwingUtilities.convertPoint(painter,
-                      loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
-
-                  val completion =
-                    new Completion_Popup(layered, loc2, font, items) {
-                      override def complete(item: Completion.Item) { insert(item) }
-                      override def propagate(evt: KeyEvent) {
-                        JEdit_Lib.propagate_key(view, evt)
-                        input(evt)
+                    val completion =
+                      new Completion_Popup(layered, loc2, font, result.items) {
+                        override def complete(item: Completion.Item) { insert(item) }
+                        override def propagate(evt: KeyEvent) {
+                          JEdit_Lib.propagate_key(view, evt)
+                          input(evt)
+                        }
+                        override def refocus() { text_area.requestFocus }
                       }
-                      override def refocus() { text_area.requestFocus }
-                    }
-                  completion_popup = Some(completion)
-                  completion.show_popup()
+                    completion_popup = Some(completion)
+                    completion.show_popup()
+                  }
                 }
               case None =>
             }