visually explicit focus (behaviour dependent on platform and look-and-feel);

--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sun Jun 30 12:40:55 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Mon Jul 01 12:01:24 2013 +0200
@@ -169,11 +169,15 @@
     }
 
   pretty_text_area.addFocusListener(new FocusAdapter {
+    override def focusGained(e: FocusEvent)
+    {
+      tip_border(3)
+    }
     override def focusLost(e: FocusEvent)
     {
       Pretty_Tooltip.hierarchy(tip) match {
         case Some((Nil, _)) => Pretty_Tooltip.dismiss(tip)
-        case _ =>
+        case _ => tip_border(1)
       }
     }
   })
@@ -184,8 +188,14 @@
 
   /* main content */
 
+  def tip_border(thickness: Int = 1)
+  {
+    tip.setBorder(new LineBorder(Color.BLACK, thickness))
+    tip.repaint()
+  }
+  tip_border(1)
+
   override def getFocusTraversalKeysEnabled = false
-  tip.setBorder(new LineBorder(Color.BLACK))
   tip.setBackground(rendering.tooltip_color)
   tip.add(controls.peer, BorderLayout.NORTH)
   tip.add(pretty_text_area)