src/Tools/jEdit/src/completion_popup.scala
changeset 53273 473ea1ed7503
parent 53272 0dfd78ff7696
child 53274 1760c01f1c78
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 10:01:59 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 10:24:43 2013 +0200
     1.3 @@ -38,6 +38,8 @@
     1.4  
     1.5    class Text_Area private(text_area: JEditTextArea, get_syntax: => Option[Outer_Syntax])
     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 @@ -54,6 +56,9 @@
    1.13        }
    1.14      }
    1.15  
    1.16 +
    1.17 +    /* insert selected item */
    1.18 +
    1.19      private def insert(item: Item)
    1.20      {
    1.21        Swing_Thread.require()
    1.22 @@ -73,65 +78,83 @@
    1.23        }
    1.24      }
    1.25  
    1.26 +
    1.27 +    /* input of key events */
    1.28 +
    1.29      def input(evt: KeyEvent)
    1.30      {
    1.31        Swing_Thread.require()
    1.32  
    1.33 -      val view = text_area.getView
    1.34 -      val layered = view.getLayeredPane
    1.35 -      val buffer = text_area.getBuffer
    1.36 -      val painter = text_area.getPainter
    1.37 -
    1.38 -      if (buffer.isEditable && !evt.isConsumed) {
    1.39 -        dismissed()
    1.40 -
    1.41 -        get_syntax match {
    1.42 -          case Some(syntax) =>
    1.43 -            val caret = text_area.getCaretPosition
    1.44 -            val result =
    1.45 -            {
    1.46 -              val line = buffer.getLineOfOffset(caret)
    1.47 -              val start = buffer.getLineStartOffset(line)
    1.48 -              val text = buffer.getSegment(start, caret - start)
    1.49 -
    1.50 -              syntax.completion.complete(text) match {
    1.51 -                case Some((word, cs)) =>
    1.52 -                  val ds =
    1.53 -                    (if (Isabelle_Encoding.is_active(buffer))
    1.54 -                      cs.map(Symbol.decode(_)).sorted
    1.55 -                     else cs).filter(_ != word)
    1.56 -                  if (ds.isEmpty) None
    1.57 -                  else Some((word, ds.map(s => Item(word, s, s))))
    1.58 -                case None => None
    1.59 -              }
    1.60 -            }
    1.61 -            result match {
    1.62 -              case Some((original, items)) =>
    1.63 -                val font = painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
    1.64 -
    1.65 -                val loc1 = text_area.offsetToXY(caret - original.length)
    1.66 -                if (loc1 != null) {
    1.67 -                  val loc2 =
    1.68 -                    SwingUtilities.convertPoint(painter,
    1.69 -                      loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
    1.70 -                  val completion =
    1.71 -                    new Completion_Popup(layered, loc2, font, items) {
    1.72 -                      override def complete(item: Item) { insert(item) }
    1.73 -                      override def propagate(e: KeyEvent) {
    1.74 -                        JEdit_Lib.propagate_key(view, e)
    1.75 -                        input(e)
    1.76 -                      }
    1.77 -                      override def refocus() { text_area.requestFocus }
    1.78 -                    }
    1.79 -                  completion_popup = Some(completion)
    1.80 -                  completion.show_popup()
    1.81 -                }
    1.82 -              case None =>
    1.83 -            }
    1.84 -          case None =>
    1.85 +      if (PIDE.options.bool("jedit_completion")) {
    1.86 +        if (!evt.isConsumed) {
    1.87 +          dismissed()
    1.88 +          input_delay.invoke()
    1.89          }
    1.90        }
    1.91 +      else {
    1.92 +        dismissed()
    1.93 +        input_delay.revoke()
    1.94 +      }
    1.95      }
    1.96 +
    1.97 +    private val input_delay =
    1.98 +      Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay"))
    1.99 +      {
   1.100 +        val view = text_area.getView
   1.101 +        val layered = view.getLayeredPane
   1.102 +        val buffer = text_area.getBuffer
   1.103 +        val painter = text_area.getPainter
   1.104 +
   1.105 +        if (buffer.isEditable) {
   1.106 +          get_syntax match {
   1.107 +            case Some(syntax) =>
   1.108 +              val caret = text_area.getCaretPosition
   1.109 +              val result =
   1.110 +              {
   1.111 +                val line = buffer.getLineOfOffset(caret)
   1.112 +                val start = buffer.getLineStartOffset(line)
   1.113 +                val text = buffer.getSegment(start, caret - start)
   1.114 +
   1.115 +                syntax.completion.complete(text) match {
   1.116 +                  case Some((word, cs)) =>
   1.117 +                    val ds =
   1.118 +                      (if (Isabelle_Encoding.is_active(buffer))
   1.119 +                        cs.map(Symbol.decode(_)).sorted
   1.120 +                       else cs).filter(_ != word)
   1.121 +                    if (ds.isEmpty) None
   1.122 +                    else Some((word, ds.map(s => Item(word, s, s))))
   1.123 +                  case None => None
   1.124 +                }
   1.125 +              }
   1.126 +              result match {
   1.127 +                case Some((original, items)) =>
   1.128 +                  val font =
   1.129 +                    painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
   1.130 +
   1.131 +                  val loc1 = text_area.offsetToXY(caret - original.length)
   1.132 +                  if (loc1 != null) {
   1.133 +                    val loc2 =
   1.134 +                      SwingUtilities.convertPoint(painter,
   1.135 +                        loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
   1.136 +
   1.137 +                    val completion =
   1.138 +                      new Completion_Popup(layered, loc2, font, items) {
   1.139 +                        override def complete(item: Item) { insert(item) }
   1.140 +                        override def propagate(e: KeyEvent) {
   1.141 +                          JEdit_Lib.propagate_key(view, e)
   1.142 +                          input(e)
   1.143 +                        }
   1.144 +                        override def refocus() { text_area.requestFocus }
   1.145 +                      }
   1.146 +                    completion_popup = Some(completion)
   1.147 +                    completion.show_popup()
   1.148 +                  }
   1.149 +                case None =>
   1.150 +              }
   1.151 +            case None =>
   1.152 +          }
   1.153 +        }
   1.154 +      }
   1.155    }
   1.156  }
   1.157