equal
deleted
inserted
replaced
120 if (new_text_info != old_text_info) { |
120 if (new_text_info != old_text_info) { |
121 if (cursor.isDefined) { |
121 if (cursor.isDefined) { |
122 if (new_text_info.isDefined) |
122 if (new_text_info.isDefined) |
123 text_area.getPainter.setCursor(Cursor.getPredefinedCursor(cursor.get)) |
123 text_area.getPainter.setCursor(Cursor.getPredefinedCursor(cursor.get)) |
124 else |
124 else |
125 text_area.getPainter.resetCursor |
125 text_area.getPainter.setCursor(Cursor.getPredefinedCursor(Cursor.TEXT_CURSOR)) |
126 } |
126 } |
127 for { |
127 for { |
128 r0 <- JEdit_Lib.visible_range(text_area) |
128 r0 <- JEdit_Lib.visible_range(text_area) |
129 opt <- List(old_text_info, new_text_info) |
129 opt <- List(old_text_info, new_text_info) |
130 (_, Text.Info(r1, _)) <- opt |
130 (_, Text.Info(r1, _)) <- opt |