# HG changeset patch
# User wenzelm
# Date 1316290395 -7200
# Node ID 86e4916825ee0f7b6bbcb6bafb52dc48c4d13367
# Parent  098dd95349e763ae982aef2aebb01a1894590900
more precise painting;

diff -r 098dd95349e7 -r 86e4916825ee src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 17 21:28:52 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 17 22:13:15 2011 +0200
@@ -96,9 +96,11 @@
     {
       nodes_status.get(node_name) match {
         case Some(st) if st.total > 0 =>
-          val w = getWidth
-          val h = getHeight
-          var end = w
+          val size = peer.getSize()
+          val insets = border.getBorderInsets(this.peer)
+          val w = size.width - insets.left - insets.right
+          val h = size.height - insets.top - insets.bottom
+          var end = size.width - insets.right
           for {
             (n, color) <- List(
               (st.unprocessed, Isabelle_Markup.unprocessed1_color),
@@ -107,7 +109,7 @@
           {
             gfx.setColor(color)
             val v = (n * w / st.total) max (if (n > 0) 2 else 0)
-            gfx.fillRect(end - v, 0, v, h)
+            gfx.fillRect(end - v, insets.top, v, h)
             end -= v
           }
         case _ =>
@@ -124,6 +126,8 @@
       name: Document.Node.Name, index: Int)
     {
       component.opaque = false
+      component.background = list.background
+      component.foreground = list.foreground
       component.node_name = name
       component.text = name.theory
     }