equal
deleted
inserted
replaced
122 Swing_Thread.require() |
122 Swing_Thread.require() |
123 val buffer_range = model.buffer_range() |
123 val buffer_range = model.buffer_range() |
124 Text.Perspective( |
124 Text.Perspective( |
125 for { |
125 for { |
126 i <- 0 until text_area.getVisibleLines |
126 i <- 0 until text_area.getVisibleLines |
127 val start = text_area.getScreenLineStartOffset(i) |
127 start = text_area.getScreenLineStartOffset(i) |
128 val stop = text_area.getScreenLineEndOffset(i) |
128 stop = text_area.getScreenLineEndOffset(i) |
129 if start >= 0 && stop >= 0 |
129 if start >= 0 && stop >= 0 |
130 val range <- buffer_range.try_restrict(Text.Range(start, stop)) |
130 range <- buffer_range.try_restrict(Text.Range(start, stop)) |
131 if !range.is_singularity |
131 if !range.is_singularity |
132 } |
132 } |
133 yield range) |
133 yield range) |
134 } |
134 } |
135 |
135 |
386 val visible_cmds = |
386 val visible_cmds = |
387 snapshot.node.command_range(snapshot.revert(visible)).map(_._1) |
387 snapshot.node.command_range(snapshot.revert(visible)).map(_._1) |
388 if (visible_cmds.exists(changed.commands)) { |
388 if (visible_cmds.exists(changed.commands)) { |
389 for { |
389 for { |
390 line <- 0 until text_area.getVisibleLines |
390 line <- 0 until text_area.getVisibleLines |
391 val start = text_area.getScreenLineStartOffset(line) if start >= 0 |
391 start = text_area.getScreenLineStartOffset(line) if start >= 0 |
392 val end = text_area.getScreenLineEndOffset(line) if end >= 0 |
392 end = text_area.getScreenLineEndOffset(line) if end >= 0 |
393 val range = proper_line_range(start, end) |
393 range = proper_line_range(start, end) |
394 val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1) |
394 line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1) |
395 if line_cmds.exists(changed.commands) |
395 if line_cmds.exists(changed.commands) |
396 } text_area.invalidateScreenLineRange(line, line) |
396 } text_area.invalidateScreenLineRange(line, line) |
397 } |
397 } |
398 } |
398 } |
399 case None => |
399 case None => |