# HG changeset patch
# User wenzelm
# Date 1334423374 -7200
# Node ID d6a1b5aeb4b149250c03254eb37abd2d0a254d83
# Parent  335a1bd767100ed179fb3dd877dbfd83777d184b
use official TextArea.isCaretVisible and thus follow the "blink" flag;
updated jedit_build component;

diff -r 335a1bd76710 -r d6a1b5aeb4b1 Admin/isatest/isatest-makedist
--- a/Admin/isatest/isatest-makedist	Sat Apr 14 18:28:11 2012 +0200
+++ b/Admin/isatest/isatest-makedist	Sat Apr 14 19:09:34 2012 +0200
@@ -59,7 +59,7 @@
 
 echo "### building distribution"  >> $DISTLOG 2>&1
 mkdir -p $DISTPREFIX
-$MAKEDIST -j "/home/isabelle/contrib_devel/jedit_build-20120327" >> $DISTLOG 2>&1
+$MAKEDIST -j "/home/isabelle/contrib_devel/jedit_build-20120414" >> $DISTLOG 2>&1
 
 if [ $? -ne 0 ]
 then
diff -r 335a1bd76710 -r d6a1b5aeb4b1 src/Tools/jEdit/README_BUILD
--- a/src/Tools/jEdit/README_BUILD	Sat Apr 14 18:28:11 2012 +0200
+++ b/src/Tools/jEdit/README_BUILD	Sat Apr 14 19:09:34 2012 +0200
@@ -12,13 +12,13 @@
   (experimental support for Scala 2.10.x milestones)
 
 * Auxiliary jedit_build component
-  http://www4.in.tum.de/~wenzelm/test/jedit_build-20120327.tar.gz
+  http://www4.in.tum.de/~wenzelm/test/jedit_build-20120414.tar.gz
 
 
 Important settings within Isabelle environment
 ==============================================
 
-* init_component ".../jedit_build-20120327"
+* init_component ".../jedit_build-20120414"
 * ISABELLE_JDK_HOME
 * SCALA_HOME
 
diff -r 335a1bd76710 -r d6a1b5aeb4b1 src/Tools/jEdit/patches/jedit-4.5.1/caret
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/jedit-4.5.1/caret	Sat Apr 14 19:09:34 2012 +0200
@@ -0,0 +1,12 @@
+diff -ru 4.5.1/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 4.5.1/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
+--- 4.5.1/jEdit/org/gjt/sp/jedit/textarea/TextArea.java	2012-03-25 18:51:47.000000000 +0200
++++ 4.5.1/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java	2012-04-14 18:37:11.000000000 +0200
+@@ -4907,7 +4907,7 @@
+ 	/**
+ 	 * Returns true if the caret is visible, false otherwise.
+ 	 */
+-	final boolean isCaretVisible()
++	public final boolean isCaretVisible()
+ 	{
+ 		return blink && hasFocus();
+ 	} //}}}
diff -r 335a1bd76710 -r d6a1b5aeb4b1 src/Tools/jEdit/src/text_area_painter.scala
--- a/src/Tools/jEdit/src/text_area_painter.scala	Sat Apr 14 18:28:11 2012 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala	Sat Apr 14 19:09:34 2012 +0200
@@ -220,7 +220,7 @@
           else chunk_font.getStringBounds(s, font_context).getWidth.toFloat
 
         val caret_range =
-          if (text_area.hasFocus) doc_view.caret_range()
+          if (text_area.isCaretVisible) doc_view.caret_range()
           else Text.Range(-1)
 
         val markup =
@@ -373,7 +373,7 @@
       screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
     {
       robust_snapshot { _ =>
-        if (text_area.hasFocus) {
+        if (text_area.isCaretVisible) {
           val caret = text_area.getCaretPosition
           if (start <= caret && caret == end - 1) {
             val painter = text_area.getPainter