src/Tools/jEdit/src/rich_text_area.scala

       if (new_text_info != old_text_info) {
         if (cursor.isDefined) {
           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)
           opt <- List(old_text_info, new_text_info)
           (_, Text.Info(r1, _)) <- opt