# HG changeset patch # User wenzelm # Date 1372672884 -7200 # Node ID d435febab3273cd5b468ae86a9fbe9ecef776cd1 # Parent cfab88cd7ba742eb121bf311f358f6c30f93fa44 visually explicit focus (behaviour dependent on platform and look-and-feel); diff -r cfab88cd7ba7 -r d435febab327 src/Tools/jEdit/src/pretty_tooltip.scala --- 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)