# HG changeset patch # User wenzelm # Date 1396429696 -7200 # Node ID 8a58a8c5a1c03180d0979b8c51bed28360793bc3 # Parent c3dbaa155ece8ac0503c7536c4b45cecfc39e033 tuned rendering -- visual indication of the status range, to make more clear when information might is out of view; diff -r c3dbaa155ece -r 8a58a8c5a1c0 src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala Tue Apr 01 23:04:22 2014 +0200 +++ b/src/Tools/jEdit/src/theories_dockable.scala Wed Apr 02 11:08:16 2014 +0200 @@ -127,7 +127,7 @@ val label = new Label { opaque = false - border = BorderFactory.createEmptyBorder() + border = BorderFactory.createLineBorder(Color.GRAY, 1) xAlignment = Alignment.Leading override def paintComponent(gfx: Graphics2D)