src/Tools/jEdit/src/completion_popup.scala
changeset 53274 1760c01f1c78
parent 53273 473ea1ed7503
child 53275 b34aac6511ab
equal deleted inserted replaced
53273:473ea1ed7503 53274:1760c01f1c78
    30 
    30 
    31   /* setup for jEdit text area */
    31   /* setup for jEdit text area */
    32 
    32 
    33   object Text_Area
    33   object Text_Area
    34   {
    34   {
    35     def apply(text_area: JEditTextArea, get_syntax: => Option[Outer_Syntax]): Text_Area =
    35     private val key = new Object
    36       new Text_Area(text_area, get_syntax)
    36 
    37   }
    37     def apply(text_area: JEditTextArea): Option[Completion_Popup.Text_Area] =
    38 
    38       text_area.getClientProperty(key) match {
    39   class Text_Area private(text_area: JEditTextArea, get_syntax: => Option[Outer_Syntax])
    39         case text_area_completion: Completion_Popup.Text_Area => Some(text_area_completion)
       
    40         case _ => None
       
    41       }
       
    42 
       
    43     def exit(text_area: JEditTextArea)
       
    44     {
       
    45       Swing_Thread.require()
       
    46       apply(text_area) match {
       
    47         case None =>
       
    48         case Some(text_area_completion) =>
       
    49           text_area_completion.deactivate()
       
    50           text_area.putClientProperty(key, null)
       
    51       }
       
    52     }
       
    53 
       
    54     def init(text_area: JEditTextArea): Completion_Popup.Text_Area =
       
    55     {
       
    56       exit(text_area)
       
    57       val text_area_completion = new Text_Area(text_area)
       
    58       text_area.putClientProperty(key, text_area_completion)
       
    59       text_area_completion.activate()
       
    60       text_area_completion
       
    61     }
       
    62 
       
    63     def dismissed(text_area: JEditTextArea): Boolean =
       
    64     {
       
    65       Swing_Thread.require()
       
    66       apply(text_area) match {
       
    67         case Some(text_area_completion) => text_area_completion.dismissed()
       
    68         case None => false
       
    69       }
       
    70     }
       
    71   }
       
    72 
       
    73   class Text_Area private(text_area: JEditTextArea)
    40   {
    74   {
    41     /* popup state */
    75     /* popup state */
    42 
    76 
    43     private var completion_popup: Option[Completion_Popup] = None
    77     private var completion_popup: Option[Completion_Popup] = None
    44 
    78 
   104         val layered = view.getLayeredPane
   138         val layered = view.getLayeredPane
   105         val buffer = text_area.getBuffer
   139         val buffer = text_area.getBuffer
   106         val painter = text_area.getPainter
   140         val painter = text_area.getPainter
   107 
   141 
   108         if (buffer.isEditable) {
   142         if (buffer.isEditable) {
   109           get_syntax match {
   143           Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
   110             case Some(syntax) =>
   144             case Some(syntax) =>
   111               val caret = text_area.getCaretPosition
   145               val caret = text_area.getCaretPosition
   112               val result =
   146               val result =
   113               {
   147               {
   114                 val line = buffer.getLineOfOffset(caret)
   148                 val line = buffer.getLineOfOffset(caret)
   153               }
   187               }
   154             case None =>
   188             case None =>
   155           }
   189           }
   156         }
   190         }
   157       }
   191       }
       
   192 
       
   193 
       
   194     /* activation */
       
   195 
       
   196     private val outer_key_listener =
       
   197       JEdit_Lib.key_listener(key_typed = input _)
       
   198 
       
   199     private def activate()
       
   200     {
       
   201       text_area.addKeyListener(outer_key_listener)
       
   202     }
       
   203 
       
   204     private def deactivate()
       
   205     {
       
   206       dismissed()
       
   207       text_area.removeKeyListener(outer_key_listener)
       
   208     }
   158   }
   209   }
   159 }
   210 }
   160 
   211 
   161 
   212 
   162 class Completion_Popup private(
   213 class Completion_Popup private(
   212   }
   263   }
   213 
   264 
   214 
   265 
   215   /* event handling */
   266   /* event handling */
   216 
   267 
   217   private val key_listener =
   268   private val inner_key_listener =
   218     JEdit_Lib.key_listener(
   269     JEdit_Lib.key_listener(
   219       key_pressed = (e: KeyEvent) =>
   270       key_pressed = (e: KeyEvent) =>
   220         {
   271         {
   221           if (!e.isConsumed) {
   272           if (!e.isConsumed) {
   222             e.getKeyCode match {
   273             e.getKeyCode match {
   238           propagate(e)
   289           propagate(e)
   239         },
   290         },
   240       key_typed = propagate _
   291       key_typed = propagate _
   241     )
   292     )
   242 
   293 
   243   list_view.peer.addKeyListener(key_listener)
   294   list_view.peer.addKeyListener(inner_key_listener)
   244 
   295 
   245   list_view.peer.addMouseListener(new MouseAdapter {
   296   list_view.peer.addMouseListener(new MouseAdapter {
   246     override def mouseClicked(e: MouseEvent) {
   297     override def mouseClicked(e: MouseEvent) {
   247       if (complete_selected()) e.consume
   298       if (complete_selected()) e.consume
   248       hide_popup()
   299       hide_popup()