1.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 17 21:28:52 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 17 22:13:15 2011 +0200
     1.3 @@ -96,9 +96,11 @@
     1.4      {
     1.5        nodes_status.get(node_name) match {
     1.6          case Some(st) if st.total > 0 =>
     1.7 -          val w = getWidth
     1.8 -          val h = getHeight
     1.9 -          var end = w
    1.10 +          val size = peer.getSize()
    1.11 +          val insets = border.getBorderInsets(this.peer)
    1.12 +          val w = size.width - insets.left - insets.right
    1.13 +          val h = size.height - insets.top - insets.bottom
    1.14 +          var end = size.width - insets.right
    1.15            for {
    1.16              (n, color) <- List(
    1.17                (st.unprocessed, Isabelle_Markup.unprocessed1_color),
    1.18 @@ -107,7 +109,7 @@
    1.19            {
    1.20              gfx.setColor(color)
    1.21              val v = (n * w / st.total) max (if (n > 0) 2 else 0)
    1.22 -            gfx.fillRect(end - v, 0, v, h)
    1.23 +            gfx.fillRect(end - v, insets.top, v, h)
    1.24              end -= v
    1.25            }
    1.26          case _ =>
    1.27 @@ -124,6 +126,8 @@
    1.28        name: Document.Node.Name, index: Int)
    1.29      {
    1.30        component.opaque = false
    1.31 +      component.background = list.background
    1.32 +      component.foreground = list.foreground
    1.33        component.node_name = name
    1.34        component.text = name.theory
    1.35      }