# HG changeset patch
# User wenzelm
# Date 1396622627 -7200
# Node ID 3610e0a7693cfc59c5405755fb5f5c8ad2fb1c96
# Parent  9cb137ec6ec8f6aa449436fc167752b0539e2e3e# Parent  8e7ebc4b30f16ef620c300c3da1e514b2320658c
merged;

diff -r 9cb137ec6ec8 -r 3610e0a7693c src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Fri Apr 04 15:56:40 2014 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Fri Apr 04 16:43:47 2014 +0200
@@ -73,7 +73,6 @@
             "(fn x => (Isabelle." ^ a ^ " (" ^ ml_make_string ^ " x); x))";
         in (K (env, body), ctxt') end));
 
-  
 
 (* type classes *)
 
diff -r 9cb137ec6ec8 -r 3610e0a7693c src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Fri Apr 04 15:56:40 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Fri Apr 04 16:43:47 2014 +0200
@@ -122,7 +122,7 @@
           if (new_text_info.isDefined)
             text_area.getPainter.setCursor(Cursor.getPredefinedCursor(cursor.get))
           else
-            text_area.getPainter.setCursor(Cursor.getPredefinedCursor(Cursor.TEXT_CURSOR))
+            text_area.getPainter.resetCursor()
         }
         for {
           r0 <- JEdit_Lib.visible_range(text_area)
diff -r 9cb137ec6ec8 -r 3610e0a7693c src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Fri Apr 04 15:56:40 2014 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Fri Apr 04 16:43:47 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
             })