# HG changeset patch
# User wenzelm
# Date 1377808850 -7200
# Node ID 64c31de7f21c100da49c107b699b0b83f91277cd
# Parent  65c60c782da564e927bb99d477f48a31a83c9105
border as for Pretty_Tooltip;

diff -r 65c60c782da5 -r 64c31de7f21c src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 22:35:50 2013 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 22:40:50 2013 +0200
@@ -9,9 +9,10 @@
 
 import isabelle._
 
-import java.awt.{Font, Point, BorderLayout, Dimension}
+import java.awt.{Color, Font, Point, BorderLayout, Dimension}
 import java.awt.event.{InputEvent, KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
 import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities}
+import javax.swing.border.LineBorder
 
 import scala.swing.{ListView, ScrollPane}
 import scala.swing.event.MouseClicked
@@ -307,7 +308,7 @@
   /* main content */
 
   override def getFocusTraversalKeysEnabled = false
-
+  completion.setBorder(new LineBorder(Color.BLACK))
   completion.add((new ScrollPane(list_view)).peer.asInstanceOf[JComponent])