tuned rendering -- visual indication of the status range, to make more clear when information might is out of view;
authorwenzelm
Wed Apr 02 11:08:16 2014 +0200 (2014-04-02)
changeset 563578a58a8c5a1c0
parent 56356 c3dbaa155ece
child 56358 ed09e5f3aedf
tuned rendering -- visual indication of the status range, to make more clear when information might is out of view;
src/Tools/jEdit/src/theories_dockable.scala
     1.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Tue Apr 01 23:04:22 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Apr 02 11:08:16 2014 +0200
     1.3 @@ -127,7 +127,7 @@
     1.4  
     1.5      val label = new Label {
     1.6        opaque = false
     1.7 -      border = BorderFactory.createEmptyBorder()
     1.8 +      border = BorderFactory.createLineBorder(Color.GRAY, 1)
     1.9        xAlignment = Alignment.Leading
    1.10  
    1.11        override def paintComponent(gfx: Graphics2D)