use official TextArea.isCaretVisible and thus follow the "blink" flag;
updated jedit_build component;
--- 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
--- 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
--- /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();
+ } //}}}
--- 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