75 Text.Range(offset - 1, offset + 1) |
75 Text.Range(offset - 1, offset + 1) |
76 else Text.Range(offset, offset + 1) |
76 else Text.Range(offset, offset + 1) |
77 } |
77 } |
78 catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) } |
78 catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) } |
79 } |
79 } |
|
80 |
|
81 |
|
82 /* proper line range */ |
|
83 |
|
84 // NB: TextArea.getScreenLineEndOffset of last line is beyond Buffer.getLength |
|
85 def proper_line_range(buffer: JEditBuffer, start: Text.Offset, end: Text.Offset): Text.Range = |
|
86 Text.Range(start, end min buffer.getLength) |
|
87 |
|
88 |
|
89 /* visible text range */ |
|
90 |
|
91 def visible_range(text_area: TextArea): Option[Text.Range] = |
|
92 { |
|
93 val buffer = text_area.getBuffer |
|
94 val n = text_area.getVisibleLines |
|
95 if (n > 0) { |
|
96 val start = text_area.getScreenLineStartOffset(0) |
|
97 val raw_end = text_area.getScreenLineEndOffset(n - 1) |
|
98 Some(proper_line_range(buffer, start, if (raw_end >= 0) raw_end else buffer.getLength)) |
|
99 } |
|
100 else None |
|
101 } |
|
102 |
|
103 def invalidate_range(text_area: TextArea, range: Text.Range) |
|
104 { |
|
105 val buffer = text_area.getBuffer |
|
106 text_area.invalidateLineRange( |
|
107 buffer.getLineOfOffset(range.start), |
|
108 buffer.getLineOfOffset(range.stop)) |
|
109 } |
80 } |
110 } |
81 |
111 |