src/Tools/jEdit/src/completion_popup.scala
changeset 53325 ffabc0083786
parent 53322 a4cd032172e0
child 53337 b3817a0e3211
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Fri Aug 30 12:59:28 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Fri Aug 30 13:24:14 2013 +0200
     1.3 @@ -108,30 +108,31 @@
     1.4  
     1.5              val decode = Isabelle_Encoding.is_active(buffer)
     1.6              syntax.completion.complete(decode, explicit, text) match {
     1.7 -              case Some((_, List(item))) if item.immediate && immediate =>
     1.8 -                insert(item)
     1.9 +              case Some(result) =>
    1.10 +                if (result.unique && result.items.head.immediate && immediate)
    1.11 +                  insert(result.items.head)
    1.12 +                else {
    1.13 +                  val font =
    1.14 +                    painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
    1.15  
    1.16 -              case Some((original, items)) =>
    1.17 -                val font =
    1.18 -                  painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
    1.19 +                  val loc1 = text_area.offsetToXY(caret - result.original.length)
    1.20 +                  if (loc1 != null) {
    1.21 +                    val loc2 =
    1.22 +                      SwingUtilities.convertPoint(painter,
    1.23 +                        loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
    1.24  
    1.25 -                val loc1 = text_area.offsetToXY(caret - original.length)
    1.26 -                if (loc1 != null) {
    1.27 -                  val loc2 =
    1.28 -                    SwingUtilities.convertPoint(painter,
    1.29 -                      loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
    1.30 -
    1.31 -                  val completion =
    1.32 -                    new Completion_Popup(layered, loc2, font, items) {
    1.33 -                      override def complete(item: Completion.Item) { insert(item) }
    1.34 -                      override def propagate(evt: KeyEvent) {
    1.35 -                        JEdit_Lib.propagate_key(view, evt)
    1.36 -                        input(evt)
    1.37 +                    val completion =
    1.38 +                      new Completion_Popup(layered, loc2, font, result.items) {
    1.39 +                        override def complete(item: Completion.Item) { insert(item) }
    1.40 +                        override def propagate(evt: KeyEvent) {
    1.41 +                          JEdit_Lib.propagate_key(view, evt)
    1.42 +                          input(evt)
    1.43 +                        }
    1.44 +                        override def refocus() { text_area.requestFocus }
    1.45                        }
    1.46 -                      override def refocus() { text_area.requestFocus }
    1.47 -                    }
    1.48 -                  completion_popup = Some(completion)
    1.49 -                  completion.show_popup()
    1.50 +                    completion_popup = Some(completion)
    1.51 +                    completion.show_popup()
    1.52 +                  }
    1.53                  }
    1.54                case None =>
    1.55              }