border as for Pretty_Tooltip;
authorwenzelm
Thu Aug 29 22:40:50 2013 +0200 (2013-08-29 ago)
changeset 5329764c31de7f21c
parent 53296 65c60c782da5
child 53298 2ad60808295c
border as for Pretty_Tooltip;
src/Tools/jEdit/src/completion_popup.scala
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 22:35:50 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 22:40:50 2013 +0200
     1.3 @@ -9,9 +9,10 @@
     1.4  
     1.5  import isabelle._
     1.6  
     1.7 -import java.awt.{Font, Point, BorderLayout, Dimension}
     1.8 +import java.awt.{Color, Font, Point, BorderLayout, Dimension}
     1.9  import java.awt.event.{InputEvent, KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
    1.10  import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities}
    1.11 +import javax.swing.border.LineBorder
    1.12  
    1.13  import scala.swing.{ListView, ScrollPane}
    1.14  import scala.swing.event.MouseClicked
    1.15 @@ -307,7 +308,7 @@
    1.16    /* main content */
    1.17  
    1.18    override def getFocusTraversalKeysEnabled = false
    1.19 -
    1.20 +  completion.setBorder(new LineBorder(Color.BLACK))
    1.21    completion.add((new ScrollPane(list_view)).peer.asInstanceOf[JComponent])
    1.22  
    1.23