src/Tools/jEdit/src/completion_popup.scala
changeset 53229 6ce8328d7912
parent 53228 f6c6688961db
child 53230 6589ff56cc3c
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 14:56:11 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 15:35:51 2013 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  import isabelle._
     1.6  
     1.7 -import java.awt.{Point, BorderLayout, Dimension}
     1.8 +import java.awt.{Font, Point, BorderLayout, Dimension}
     1.9  import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
    1.10  import javax.swing.{JPanel, JComponent, PopupFactory, SwingUtilities}
    1.11  
    1.12 @@ -27,16 +27,19 @@
    1.13  
    1.14    def apply(
    1.15      opt_view: Option[View],
    1.16 -    parent: JComponent,
    1.17 +    root: JComponent,
    1.18 +    popup_font: Font,
    1.19      screen_point: Point,
    1.20      items: List[Item],
    1.21 -    complete: Item => Unit): Completion_Popup =
    1.22 +    complete: Item => Unit,
    1.23 +    hidden: () => Unit): Completion_Popup =
    1.24    {
    1.25      Swing_Thread.require()
    1.26  
    1.27      require(!items.isEmpty)
    1.28  
    1.29 -    val completion = new Completion_Popup(opt_view, parent, screen_point, items, complete)
    1.30 +    val completion =
    1.31 +      new Completion_Popup(opt_view, root, popup_font, screen_point, items, complete, hidden)
    1.32      completion.show_popup()
    1.33      completion
    1.34    }
    1.35 @@ -47,20 +50,30 @@
    1.36  
    1.37      val buffer = text_area.getBuffer
    1.38      if (buffer.isEditable) {
    1.39 +      val view = text_area.getView
    1.40        val painter = text_area.getPainter
    1.41        val caret = text_area.getCaretPosition
    1.42  
    1.43        // FIXME
    1.44        def complete(item: Item) { }
    1.45 +
    1.46 +      def hidden() { text_area.requestFocus }
    1.47 +
    1.48 +      // FIXME
    1.49        val token_length = 0
    1.50        val items: List[Item] = Nil
    1.51  
    1.52 +      val popup_font =
    1.53 +        painter.getFont.deriveFont(
    1.54 +          (painter.getFont.getSize2D * PIDE.options.real("jedit_popup_font_scale")).toFloat
    1.55 +            max 10.0f)
    1.56 +
    1.57        if (!items.isEmpty) {
    1.58          val location = text_area.offsetToXY(caret - token_length)
    1.59          if (location != null) {
    1.60            location.y = location.y + painter.getFontMetrics.getHeight
    1.61            SwingUtilities.convertPointToScreen(location, painter)
    1.62 -          apply(Some(text_area.getView), painter, location, items, complete _)
    1.63 +          apply(Some(view), view.getRootPane, popup_font, location, items, complete _, hidden _)
    1.64          }
    1.65        }
    1.66      }
    1.67 @@ -70,10 +83,12 @@
    1.68  
    1.69  class Completion_Popup private(
    1.70    opt_view: Option[View],
    1.71 -  parent: JComponent,
    1.72 +  root: JComponent,
    1.73 +  popup_font: Font,
    1.74    screen_point: Point,
    1.75    items: List[Completion_Popup.Item],
    1.76 -  complete: Completion_Popup.Item => Unit) extends JPanel(new BorderLayout)
    1.77 +  complete: Completion_Popup.Item => Unit,
    1.78 +  hidden: () => Unit) extends JPanel(new BorderLayout)
    1.79  {
    1.80    completion =>
    1.81  
    1.82 @@ -84,7 +99,7 @@
    1.83  
    1.84    private val list_view = new ListView(items)
    1.85    {
    1.86 -    font = parent.getFont
    1.87 +    font = popup_font
    1.88    }
    1.89    list_view.selection.intervalMode = ListView.IntervalMode.Single
    1.90    list_view.peer.setFocusTraversalKeysEnabled(false)
    1.91 @@ -198,7 +213,7 @@
    1.92  
    1.93      val x = screen_point.x min (screen_bounds.x + screen_bounds.width - w)
    1.94      val y = screen_point.y min (screen_bounds.y + screen_bounds.height - h)
    1.95 -    PopupFactory.getSharedInstance.getPopup(parent, completion, x, y)
    1.96 +    PopupFactory.getSharedInstance.getPopup(root, completion, x, y)
    1.97    }
    1.98  
    1.99    def show_popup()
   1.100 @@ -211,18 +226,12 @@
   1.101    def hide_popup()
   1.102    {
   1.103      opt_view match {
   1.104 -      case Some(view) =>
   1.105 -        if (view.getKeyEventInterceptor == key_listener)
   1.106 -          view.setKeyEventInterceptor(null)
   1.107 -        popup.hide
   1.108 -        view.getTextArea match {
   1.109 -          case null =>
   1.110 -          case text_area => text_area.requestFocus
   1.111 -        }
   1.112 -      case None =>
   1.113 -        popup.hide
   1.114 -        parent.requestFocus
   1.115 +      case Some(view) if (view.getKeyEventInterceptor == key_listener) =>
   1.116 +        view.setKeyEventInterceptor(null)
   1.117 +      case _ =>
   1.118      }
   1.119 +    popup.hide
   1.120 +    hidden()
   1.121    }
   1.122  }
   1.123