--- a/src/Tools/jEdit/src/document_view.scala Tue Jun 14 21:41:00 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Wed Jun 15 11:41:49 2011 +0200
@@ -396,6 +396,7 @@
painter.addMouseMotionListener(mouse_motion_listener)
text_area.addCaretListener(caret_listener)
text_area.addLeftOfScrollBar(overview)
+ if (text_area.isCaretBlinkEnabled) text_area.setCaretBlinkEnabled(false)
session.commands_changed += main_actor
session.global_settings += main_actor
}
@@ -405,6 +406,7 @@
val painter = text_area.getPainter
session.commands_changed -= main_actor
session.global_settings -= main_actor
+ text_area.setCaretBlinkEnabled(jEdit.getBooleanProperty("view.caretBlink"))
text_area.removeFocusListener(focus_listener)
text_area.getView.removeWindowListener(window_listener)
painter.removeMouseMotionListener(mouse_motion_listener)