more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
authorwenzelm
Fri Aug 30 13:24:14 2013 +0200 (2013-08-30 ago)
changeset 53325ffabc0083786
parent 53324 c12a3edcd8e4
child 53326 d8ad101cc684
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
src/Pure/Isar/completion.scala
src/Tools/jEdit/src/completion_popup.scala
     1.1 --- a/src/Pure/Isar/completion.scala	Fri Aug 30 12:59:28 2013 +0200
     1.2 +++ b/src/Pure/Isar/completion.scala	Fri Aug 30 13:24:14 2013 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  
     1.5  object Completion
     1.6  {
     1.7 -  /* items */
     1.8 +  /* result */
     1.9  
    1.10    sealed case class Item(
    1.11      original: String,
    1.12 @@ -20,6 +20,8 @@
    1.13      immediate: Boolean)
    1.14    { override def toString: String = description }
    1.15  
    1.16 +  sealed case class Result(original: String, unique: Boolean, items: List[Item])
    1.17 +
    1.18  
    1.19    /* init */
    1.20  
    1.21 @@ -92,8 +94,7 @@
    1.22  
    1.23    /* complete */
    1.24  
    1.25 -  def complete(decode: Boolean, explicit: Boolean, line: CharSequence)
    1.26 -    : Option[(String, List[Completion.Item])] =
    1.27 +  def complete(decode: Boolean, explicit: Boolean, line: CharSequence): Option[Completion.Result] =
    1.28    {
    1.29      val raw_result =
    1.30        abbrevs_lex.parse(abbrevs_lex.keyword, new Library.Reverse(line)) match {
    1.31 @@ -115,13 +116,14 @@
    1.32        }
    1.33      raw_result match {
    1.34        case Some((word, cs)) =>
    1.35 -        val ds = (if (decode) cs.map(Symbol.decode(_)).sorted else cs)
    1.36 +        val ds = (if (decode) cs.map(Symbol.decode(_)).sorted else cs).filter(_ != word)
    1.37          if (ds.isEmpty) None
    1.38          else {
    1.39            val immediate =
    1.40              !Completion.is_word(word) &&
    1.41              Character.codePointCount(word, 0, word.length) > 1
    1.42 -          Some((word, ds.map(s => Completion.Item(word, s, s, explicit || immediate))))
    1.43 +          val items = ds.map(s => Completion.Item(word, s, s, explicit || immediate))
    1.44 +          Some(Completion.Result(word, cs.length == 1, items))
    1.45          }
    1.46        case None => None
    1.47      }
     2.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Fri Aug 30 12:59:28 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Fri Aug 30 13:24:14 2013 +0200
     2.3 @@ -108,30 +108,31 @@
     2.4  
     2.5              val decode = Isabelle_Encoding.is_active(buffer)
     2.6              syntax.completion.complete(decode, explicit, text) match {
     2.7 -              case Some((_, List(item))) if item.immediate && immediate =>
     2.8 -                insert(item)
     2.9 +              case Some(result) =>
    2.10 +                if (result.unique && result.items.head.immediate && immediate)
    2.11 +                  insert(result.items.head)
    2.12 +                else {
    2.13 +                  val font =
    2.14 +                    painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
    2.15  
    2.16 -              case Some((original, items)) =>
    2.17 -                val font =
    2.18 -                  painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
    2.19 +                  val loc1 = text_area.offsetToXY(caret - result.original.length)
    2.20 +                  if (loc1 != null) {
    2.21 +                    val loc2 =
    2.22 +                      SwingUtilities.convertPoint(painter,
    2.23 +                        loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
    2.24  
    2.25 -                val loc1 = text_area.offsetToXY(caret - original.length)
    2.26 -                if (loc1 != null) {
    2.27 -                  val loc2 =
    2.28 -                    SwingUtilities.convertPoint(painter,
    2.29 -                      loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
    2.30 -
    2.31 -                  val completion =
    2.32 -                    new Completion_Popup(layered, loc2, font, items) {
    2.33 -                      override def complete(item: Completion.Item) { insert(item) }
    2.34 -                      override def propagate(evt: KeyEvent) {
    2.35 -                        JEdit_Lib.propagate_key(view, evt)
    2.36 -                        input(evt)
    2.37 +                    val completion =
    2.38 +                      new Completion_Popup(layered, loc2, font, result.items) {
    2.39 +                        override def complete(item: Completion.Item) { insert(item) }
    2.40 +                        override def propagate(evt: KeyEvent) {
    2.41 +                          JEdit_Lib.propagate_key(view, evt)
    2.42 +                          input(evt)
    2.43 +                        }
    2.44 +                        override def refocus() { text_area.requestFocus }
    2.45                        }
    2.46 -                      override def refocus() { text_area.requestFocus }
    2.47 -                    }
    2.48 -                  completion_popup = Some(completion)
    2.49 -                  completion.show_popup()
    2.50 +                    completion_popup = Some(completion)
    2.51 +                    completion.show_popup()
    2.52 +                  }
    2.53                  }
    2.54                case None =>
    2.55              }