# HG changeset patch
# User wenzelm
# Date 1396619900 -7200
# Node ID 8e7ebc4b30f16ef620c300c3da1e514b2320658c
# Parent  0e21270952c319658a51d833f2e78f213f9d8dd5
tuned rendering -- take 1px line border into account;

diff -r 0e21270952c3 -r 8e7ebc4b30f1 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Fri Apr 04 14:31:31 2014 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Fri Apr 04 15:58:20 2014 +0200
@@ -160,8 +160,8 @@
                 (st.failed, PIDE.options.color_value("error_color"))
               ).filter(_._1 > 0)
 
-            (size.width /: segments)({ case (last, (n, color)) =>
-              val w = (n * (size.width - segments.length) / st.total) max 4
+            ((size.width - 1) /: segments)({ case (last, (n, color)) =>
+              val w = (n * ((size.width - 2) - segments.length) / st.total) max 4
               paint_segment(last - w, w, color)
               last - w - 1
             })