# HG changeset patch
# User wenzelm
# Date 1372678767 -7200
# Node ID ee7218d281595e15cd89013fd4de1bd25637ff2a
# Parent  0f0f80e41581c2a44833406a49cb7f35bf80f30b
less intrusive border, notably on windows;

diff -r 0f0f80e41581 -r ee7218d28159 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Mon Jul 01 13:32:26 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Mon Jul 01 13:39:27 2013 +0200
@@ -171,13 +171,13 @@
   pretty_text_area.addFocusListener(new FocusAdapter {
     override def focusGained(e: FocusEvent)
     {
-      tip_border(3)
+      tip_border(true)
     }
     override def focusLost(e: FocusEvent)
     {
       Pretty_Tooltip.hierarchy(tip) match {
         case Some((Nil, _)) => Pretty_Tooltip.dismiss(tip)
-        case _ => tip_border(1)
+        case _ => tip_border(false)
       }
     }
   })
@@ -188,12 +188,12 @@
 
   /* main content */
 
-  def tip_border(thickness: Int = 1)
+  def tip_border(has_focus: Boolean)
   {
-    tip.setBorder(new LineBorder(Color.BLACK, thickness))
+    tip.setBorder(new LineBorder(if (has_focus) Color.BLACK else Color.GRAY))
     tip.repaint()
   }
-  tip_border(1)
+  tip_border(true)
 
   override def getFocusTraversalKeysEnabled = false
   tip.setBackground(rendering.tooltip_color)