tuned;
authorwenzelm
Tue Mar 26 14:03:31 2013 +0100 (2013-03-26)
changeset 51535f2f480bc4223
parent 51534 123bd97fcea1
child 51536 a1d324ef12d4
tuned;
src/Tools/jEdit/src/theories_dockable.scala
     1.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Tue Mar 26 12:40:51 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Tue Mar 26 14:03:31 2013 +0100
     1.3 @@ -93,7 +93,7 @@
     1.4              (st.failed, PIDE.options.color_value("error_color")))
     1.5  
     1.6            val size = peer.getSize()
     1.7 -          val insets = border.getBorderInsets(this.peer)
     1.8 +          val insets = border.getBorderInsets(peer)
     1.9            val w = size.width - insets.left - insets.right
    1.10            val h = size.height - insets.top - insets.bottom
    1.11            var end = size.width - insets.right