src/Tools/jEdit/src/pretty_tooltip.scala

     }
 
   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)
       }
     }
   })
 
   pretty_text_area.resize(Rendering.font_family(),
     Rendering.font_size("jedit_tooltip_font_scale").round)
 
 
   /* main content */
 
-  def tip_border(thickness: Int = 1)
-  {
-    tip.setBorder(new LineBorder(Color.BLACK, thickness))
+  def tip_border(has_focus: Boolean)
+  {
+    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)
   tip.add(controls.peer, BorderLayout.NORTH)
   tip.add(pretty_text_area)