src/Tools/jEdit/src/completion_popup.scala
changeset 53292 f567c1c7b180
parent 53275 b34aac6511ab
child 53293 fd27b8f5a479
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 20:46:55 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 21:17:46 2013 +0200
     1.3 @@ -66,26 +66,10 @@
     1.4  
     1.5    class Text_Area private(text_area: JEditTextArea)
     1.6    {
     1.7 -    /* popup state */
     1.8 -
     1.9      private var completion_popup: Option[Completion_Popup] = None
    1.10  
    1.11 -    def dismissed(): Boolean =
    1.12 -    {
    1.13 -      Swing_Thread.require()
    1.14  
    1.15 -      completion_popup match {
    1.16 -        case Some(completion) =>
    1.17 -          completion.hide_popup()
    1.18 -          completion_popup = None
    1.19 -          true
    1.20 -        case None =>
    1.21 -          false
    1.22 -      }
    1.23 -    }
    1.24 -
    1.25 -
    1.26 -    /* insert selected item */
    1.27 +    /* completion action */
    1.28  
    1.29      private def insert(item: Completion.Item)
    1.30      {
    1.31 @@ -106,8 +90,56 @@
    1.32        }
    1.33      }
    1.34  
    1.35 +    def action(immediate: Boolean)
    1.36 +    {
    1.37 +      val view = text_area.getView
    1.38 +      val layered = view.getLayeredPane
    1.39 +      val buffer = text_area.getBuffer
    1.40 +      val painter = text_area.getPainter
    1.41  
    1.42 -    /* input of key events */
    1.43 +      if (buffer.isEditable) {
    1.44 +        Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
    1.45 +          case Some(syntax) =>
    1.46 +            val caret = text_area.getCaretPosition
    1.47 +            val line = buffer.getLineOfOffset(caret)
    1.48 +            val start = buffer.getLineStartOffset(line)
    1.49 +            val text = buffer.getSegment(start, caret - start)
    1.50 +
    1.51 +            syntax.completion.complete(Isabelle_Encoding.is_active(buffer), text) match {
    1.52 +              case Some((_, List(item))) if immediate =>
    1.53 +                insert(item)
    1.54 +
    1.55 +              case Some((original, items)) =>
    1.56 +                val font =
    1.57 +                  painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
    1.58 +
    1.59 +                val loc1 = text_area.offsetToXY(caret - original.length)
    1.60 +                if (loc1 != null) {
    1.61 +                  val loc2 =
    1.62 +                    SwingUtilities.convertPoint(painter,
    1.63 +                      loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
    1.64 +
    1.65 +                  val completion =
    1.66 +                    new Completion_Popup(layered, loc2, font, items) {
    1.67 +                      override def complete(item: Completion.Item) { insert(item) }
    1.68 +                      override def propagate(evt: KeyEvent) {
    1.69 +                        JEdit_Lib.propagate_key(view, evt)
    1.70 +                        input(evt)
    1.71 +                      }
    1.72 +                      override def refocus() { text_area.requestFocus }
    1.73 +                    }
    1.74 +                  completion_popup = Some(completion)
    1.75 +                  completion.show_popup()
    1.76 +                }
    1.77 +              case None =>
    1.78 +            }
    1.79 +          case None =>
    1.80 +        }
    1.81 +      }
    1.82 +    }
    1.83 +
    1.84 +
    1.85 +    /* input key events */
    1.86  
    1.87      def input(evt: KeyEvent)
    1.88      {
    1.89 @@ -116,7 +148,11 @@
    1.90        if (PIDE.options.bool("jedit_completion")) {
    1.91          if (!evt.isConsumed) {
    1.92            dismissed()
    1.93 -          input_delay.invoke()
    1.94 +          if (PIDE.options.seconds("jedit_completion_delay").is_zero) {
    1.95 +            input_delay.revoke()
    1.96 +            action(PIDE.options.bool("jedit_completion_immediate"))
    1.97 +          }
    1.98 +          else input_delay.invoke()
    1.99          }
   1.100        }
   1.101        else {
   1.102 @@ -126,50 +162,26 @@
   1.103      }
   1.104  
   1.105      private val input_delay =
   1.106 -      Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay"))
   1.107 -      {
   1.108 -        val view = text_area.getView
   1.109 -        val layered = view.getLayeredPane
   1.110 -        val buffer = text_area.getBuffer
   1.111 -        val painter = text_area.getPainter
   1.112 +      Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
   1.113 +        action(false)
   1.114 +      }
   1.115  
   1.116 -        if (buffer.isEditable) {
   1.117 -          Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
   1.118 -            case Some(syntax) =>
   1.119 -              val caret = text_area.getCaretPosition
   1.120 -              val line = buffer.getLineOfOffset(caret)
   1.121 -              val start = buffer.getLineStartOffset(line)
   1.122 -              val text = buffer.getSegment(start, caret - start)
   1.123  
   1.124 -              syntax.completion.complete(Isabelle_Encoding.is_active(buffer), text) match {
   1.125 -                case Some((original, items)) =>
   1.126 -                  val font =
   1.127 -                    painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
   1.128 +    /* dismiss popup */
   1.129  
   1.130 -                  val loc1 = text_area.offsetToXY(caret - original.length)
   1.131 -                  if (loc1 != null) {
   1.132 -                    val loc2 =
   1.133 -                      SwingUtilities.convertPoint(painter,
   1.134 -                        loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
   1.135 +    def dismissed(): Boolean =
   1.136 +    {
   1.137 +      Swing_Thread.require()
   1.138  
   1.139 -                    val completion =
   1.140 -                      new Completion_Popup(layered, loc2, font, items) {
   1.141 -                        override def complete(item: Completion.Item) { insert(item) }
   1.142 -                        override def propagate(evt: KeyEvent) {
   1.143 -                          JEdit_Lib.propagate_key(view, evt)
   1.144 -                          input(evt)
   1.145 -                        }
   1.146 -                        override def refocus() { text_area.requestFocus }
   1.147 -                      }
   1.148 -                    completion_popup = Some(completion)
   1.149 -                    completion.show_popup()
   1.150 -                  }
   1.151 -                case None =>
   1.152 -              }
   1.153 -            case None =>
   1.154 -          }
   1.155 -        }
   1.156 +      completion_popup match {
   1.157 +        case Some(completion) =>
   1.158 +          completion.hide_popup()
   1.159 +          completion_popup = None
   1.160 +          true
   1.161 +        case None =>
   1.162 +          false
   1.163        }
   1.164 +    }
   1.165  
   1.166  
   1.167      /* activation */