src/Tools/jEdit/src/completion_popup.scala
changeset 53274 1760c01f1c78
parent 53273 473ea1ed7503
child 53275 b34aac6511ab
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 10:24:43 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 12:38:33 2013 +0200
     1.3 @@ -32,11 +32,45 @@
     1.4  
     1.5    object Text_Area
     1.6    {
     1.7 -    def apply(text_area: JEditTextArea, get_syntax: => Option[Outer_Syntax]): Text_Area =
     1.8 -      new Text_Area(text_area, get_syntax)
     1.9 +    private val key = new Object
    1.10 +
    1.11 +    def apply(text_area: JEditTextArea): Option[Completion_Popup.Text_Area] =
    1.12 +      text_area.getClientProperty(key) match {
    1.13 +        case text_area_completion: Completion_Popup.Text_Area => Some(text_area_completion)
    1.14 +        case _ => None
    1.15 +      }
    1.16 +
    1.17 +    def exit(text_area: JEditTextArea)
    1.18 +    {
    1.19 +      Swing_Thread.require()
    1.20 +      apply(text_area) match {
    1.21 +        case None =>
    1.22 +        case Some(text_area_completion) =>
    1.23 +          text_area_completion.deactivate()
    1.24 +          text_area.putClientProperty(key, null)
    1.25 +      }
    1.26 +    }
    1.27 +
    1.28 +    def init(text_area: JEditTextArea): Completion_Popup.Text_Area =
    1.29 +    {
    1.30 +      exit(text_area)
    1.31 +      val text_area_completion = new Text_Area(text_area)
    1.32 +      text_area.putClientProperty(key, text_area_completion)
    1.33 +      text_area_completion.activate()
    1.34 +      text_area_completion
    1.35 +    }
    1.36 +
    1.37 +    def dismissed(text_area: JEditTextArea): Boolean =
    1.38 +    {
    1.39 +      Swing_Thread.require()
    1.40 +      apply(text_area) match {
    1.41 +        case Some(text_area_completion) => text_area_completion.dismissed()
    1.42 +        case None => false
    1.43 +      }
    1.44 +    }
    1.45    }
    1.46  
    1.47 -  class Text_Area private(text_area: JEditTextArea, get_syntax: => Option[Outer_Syntax])
    1.48 +  class Text_Area private(text_area: JEditTextArea)
    1.49    {
    1.50      /* popup state */
    1.51  
    1.52 @@ -106,7 +140,7 @@
    1.53          val painter = text_area.getPainter
    1.54  
    1.55          if (buffer.isEditable) {
    1.56 -          get_syntax match {
    1.57 +          Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
    1.58              case Some(syntax) =>
    1.59                val caret = text_area.getCaretPosition
    1.60                val result =
    1.61 @@ -155,6 +189,23 @@
    1.62            }
    1.63          }
    1.64        }
    1.65 +
    1.66 +
    1.67 +    /* activation */
    1.68 +
    1.69 +    private val outer_key_listener =
    1.70 +      JEdit_Lib.key_listener(key_typed = input _)
    1.71 +
    1.72 +    private def activate()
    1.73 +    {
    1.74 +      text_area.addKeyListener(outer_key_listener)
    1.75 +    }
    1.76 +
    1.77 +    private def deactivate()
    1.78 +    {
    1.79 +      dismissed()
    1.80 +      text_area.removeKeyListener(outer_key_listener)
    1.81 +    }
    1.82    }
    1.83  }
    1.84  
    1.85 @@ -214,7 +265,7 @@
    1.86  
    1.87    /* event handling */
    1.88  
    1.89 -  private val key_listener =
    1.90 +  private val inner_key_listener =
    1.91      JEdit_Lib.key_listener(
    1.92        key_pressed = (e: KeyEvent) =>
    1.93          {
    1.94 @@ -240,7 +291,7 @@
    1.95        key_typed = propagate _
    1.96      )
    1.97  
    1.98 -  list_view.peer.addKeyListener(key_listener)
    1.99 +  list_view.peer.addKeyListener(inner_key_listener)
   1.100  
   1.101    list_view.peer.addMouseListener(new MouseAdapter {
   1.102      override def mouseClicked(e: MouseEvent) {