option to insert unique completion immediately into buffer;
authorwenzelm
Thu Aug 29 21:17:46 2013 +0200 (2013-08-29 ago)
changeset 53292f567c1c7b180
parent 53291 f7fa953bd15b
child 53293 fd27b8f5a479
option to insert unique completion immediately into buffer;
src/Pure/General/time.scala
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/completion_popup.scala
     1.1 --- a/src/Pure/General/time.scala	Thu Aug 29 20:46:55 2013 +0200
     1.2 +++ b/src/Pure/General/time.scala	Thu Aug 29 21:17:46 2013 +0200
     1.3 @@ -30,6 +30,7 @@
     1.4    def min(t: Time): Time = if (ms < t.ms) this else t
     1.5    def max(t: Time): Time = if (ms > t.ms) this else t
     1.6  
     1.7 +  def is_zero: Boolean = ms == 0
     1.8    def is_relevant: Boolean = ms >= 1
     1.9  
    1.10    override def hashCode: Int = ms.hashCode
     2.1 --- a/src/Tools/jEdit/etc/options	Thu Aug 29 20:46:55 2013 +0200
     2.2 +++ b/src/Tools/jEdit/etc/options	Thu Aug 29 21:17:46 2013 +0200
     2.3 @@ -39,6 +39,9 @@
     2.4  public option jedit_completion_delay : real = 0.0
     2.5    -- "delay for completion popup (seconds)"
     2.6  
     2.7 +public option jedit_completion_immediate : bool = false
     2.8 +  -- "insert unique completion immediately into buffer (if delay = 0)"
     2.9 +
    2.10  
    2.11  section "Rendering of Document Content"
    2.12  
     3.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 20:46:55 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 21:17:46 2013 +0200
     3.3 @@ -66,26 +66,10 @@
     3.4  
     3.5    class Text_Area private(text_area: JEditTextArea)
     3.6    {
     3.7 -    /* popup state */
     3.8 -
     3.9      private var completion_popup: Option[Completion_Popup] = None
    3.10  
    3.11 -    def dismissed(): Boolean =
    3.12 -    {
    3.13 -      Swing_Thread.require()
    3.14  
    3.15 -      completion_popup match {
    3.16 -        case Some(completion) =>
    3.17 -          completion.hide_popup()
    3.18 -          completion_popup = None
    3.19 -          true
    3.20 -        case None =>
    3.21 -          false
    3.22 -      }
    3.23 -    }
    3.24 -
    3.25 -
    3.26 -    /* insert selected item */
    3.27 +    /* completion action */
    3.28  
    3.29      private def insert(item: Completion.Item)
    3.30      {
    3.31 @@ -106,8 +90,56 @@
    3.32        }
    3.33      }
    3.34  
    3.35 +    def action(immediate: Boolean)
    3.36 +    {
    3.37 +      val view = text_area.getView
    3.38 +      val layered = view.getLayeredPane
    3.39 +      val buffer = text_area.getBuffer
    3.40 +      val painter = text_area.getPainter
    3.41  
    3.42 -    /* input of key events */
    3.43 +      if (buffer.isEditable) {
    3.44 +        Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
    3.45 +          case Some(syntax) =>
    3.46 +            val caret = text_area.getCaretPosition
    3.47 +            val line = buffer.getLineOfOffset(caret)
    3.48 +            val start = buffer.getLineStartOffset(line)
    3.49 +            val text = buffer.getSegment(start, caret - start)
    3.50 +
    3.51 +            syntax.completion.complete(Isabelle_Encoding.is_active(buffer), text) match {
    3.52 +              case Some((_, List(item))) if immediate =>
    3.53 +                insert(item)
    3.54 +
    3.55 +              case Some((original, items)) =>
    3.56 +                val font =
    3.57 +                  painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
    3.58 +
    3.59 +                val loc1 = text_area.offsetToXY(caret - original.length)
    3.60 +                if (loc1 != null) {
    3.61 +                  val loc2 =
    3.62 +                    SwingUtilities.convertPoint(painter,
    3.63 +                      loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
    3.64 +
    3.65 +                  val completion =
    3.66 +                    new Completion_Popup(layered, loc2, font, items) {
    3.67 +                      override def complete(item: Completion.Item) { insert(item) }
    3.68 +                      override def propagate(evt: KeyEvent) {
    3.69 +                        JEdit_Lib.propagate_key(view, evt)
    3.70 +                        input(evt)
    3.71 +                      }
    3.72 +                      override def refocus() { text_area.requestFocus }
    3.73 +                    }
    3.74 +                  completion_popup = Some(completion)
    3.75 +                  completion.show_popup()
    3.76 +                }
    3.77 +              case None =>
    3.78 +            }
    3.79 +          case None =>
    3.80 +        }
    3.81 +      }
    3.82 +    }
    3.83 +
    3.84 +
    3.85 +    /* input key events */
    3.86  
    3.87      def input(evt: KeyEvent)
    3.88      {
    3.89 @@ -116,7 +148,11 @@
    3.90        if (PIDE.options.bool("jedit_completion")) {
    3.91          if (!evt.isConsumed) {
    3.92            dismissed()
    3.93 -          input_delay.invoke()
    3.94 +          if (PIDE.options.seconds("jedit_completion_delay").is_zero) {
    3.95 +            input_delay.revoke()
    3.96 +            action(PIDE.options.bool("jedit_completion_immediate"))
    3.97 +          }
    3.98 +          else input_delay.invoke()
    3.99          }
   3.100        }
   3.101        else {
   3.102 @@ -126,50 +162,26 @@
   3.103      }
   3.104  
   3.105      private val input_delay =
   3.106 -      Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay"))
   3.107 -      {
   3.108 -        val view = text_area.getView
   3.109 -        val layered = view.getLayeredPane
   3.110 -        val buffer = text_area.getBuffer
   3.111 -        val painter = text_area.getPainter
   3.112 +      Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
   3.113 +        action(false)
   3.114 +      }
   3.115  
   3.116 -        if (buffer.isEditable) {
   3.117 -          Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
   3.118 -            case Some(syntax) =>
   3.119 -              val caret = text_area.getCaretPosition
   3.120 -              val line = buffer.getLineOfOffset(caret)
   3.121 -              val start = buffer.getLineStartOffset(line)
   3.122 -              val text = buffer.getSegment(start, caret - start)
   3.123  
   3.124 -              syntax.completion.complete(Isabelle_Encoding.is_active(buffer), text) match {
   3.125 -                case Some((original, items)) =>
   3.126 -                  val font =
   3.127 -                    painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
   3.128 +    /* dismiss popup */
   3.129  
   3.130 -                  val loc1 = text_area.offsetToXY(caret - original.length)
   3.131 -                  if (loc1 != null) {
   3.132 -                    val loc2 =
   3.133 -                      SwingUtilities.convertPoint(painter,
   3.134 -                        loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
   3.135 +    def dismissed(): Boolean =
   3.136 +    {
   3.137 +      Swing_Thread.require()
   3.138  
   3.139 -                    val completion =
   3.140 -                      new Completion_Popup(layered, loc2, font, items) {
   3.141 -                        override def complete(item: Completion.Item) { insert(item) }
   3.142 -                        override def propagate(evt: KeyEvent) {
   3.143 -                          JEdit_Lib.propagate_key(view, evt)
   3.144 -                          input(evt)
   3.145 -                        }
   3.146 -                        override def refocus() { text_area.requestFocus }
   3.147 -                      }
   3.148 -                    completion_popup = Some(completion)
   3.149 -                    completion.show_popup()
   3.150 -                  }
   3.151 -                case None =>
   3.152 -              }
   3.153 -            case None =>
   3.154 -          }
   3.155 -        }
   3.156 +      completion_popup match {
   3.157 +        case Some(completion) =>
   3.158 +          completion.hide_popup()
   3.159 +          completion_popup = None
   3.160 +          true
   3.161 +        case None =>
   3.162 +          false
   3.163        }
   3.164 +    }
   3.165  
   3.166  
   3.167      /* activation */