107 } |
107 } |
108 catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) } |
108 catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) } |
109 } |
109 } |
110 |
110 |
111 |
111 |
112 /* proper line range */ |
|
113 |
|
114 // NB: TextArea.getScreenLineEndOffset of last line is beyond Buffer.getLength |
|
115 def proper_line_range(buffer: JEditBuffer, start: Text.Offset, end: Text.Offset): Text.Range = |
|
116 Text.Range(start, end min buffer.getLength) |
|
117 |
|
118 |
|
119 /* visible text range */ |
112 /* visible text range */ |
120 |
113 |
121 def visible_range(text_area: TextArea): Option[Text.Range] = |
114 def visible_range(text_area: TextArea): Option[Text.Range] = |
122 { |
115 { |
123 val buffer = text_area.getBuffer |
116 val buffer = text_area.getBuffer |
124 val n = text_area.getVisibleLines |
117 val n = text_area.getVisibleLines |
125 if (n > 0) { |
118 if (n > 0) { |
126 val start = text_area.getScreenLineStartOffset(0) |
119 val start = text_area.getScreenLineStartOffset(0) |
127 val raw_end = text_area.getScreenLineEndOffset(n - 1) |
120 val raw_end = text_area.getScreenLineEndOffset(n - 1) |
128 Some(proper_line_range(buffer, start, if (raw_end >= 0) raw_end else buffer.getLength)) |
121 val end = if (raw_end >= 0) raw_end min buffer.getLength else buffer.getLength |
|
122 Some(Text.Range(start, end)) |
129 } |
123 } |
130 else None |
124 else None |
131 } |
125 } |
132 |
126 |
133 def invalidate_range(text_area: TextArea, range: Text.Range) |
127 def invalidate_range(text_area: TextArea, range: Text.Range) |
152 |
146 |
153 /* graphics range */ |
147 /* graphics range */ |
154 |
148 |
155 class Gfx_Range(val x: Int, val y: Int, val length: Int) |
149 class Gfx_Range(val x: Int, val y: Int, val length: Int) |
156 |
150 |
157 // NB: jEdit already normalizes \r\n and \r to \n |
151 // NB: jEdit always normalizes \r\n and \r to \n |
158 // NB: last line lacks \n |
152 // NB: last line lacks \n |
159 def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] = |
153 def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] = |
160 { |
154 { |
161 val buffer = text_area.getBuffer |
155 val buffer = text_area.getBuffer |
162 |
156 |
163 val p = text_area.offsetToXY(range.start) |
157 val p = text_area.offsetToXY(range.start) |
164 |
158 |
165 val end = buffer.getLength |
159 val end = buffer.getLength |
166 val stop = range.stop |
160 val stop = range.stop |
167 val (q, r) = |
161 val (q, r) = |
168 if (stop >= end) (text_area.offsetToXY(end), char_width(text_area)) |
162 if (stop >= end) (text_area.offsetToXY(end), char_width(text_area) * (stop - end)) |
169 else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n") |
163 else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n") |
170 (text_area.offsetToXY(stop - 1), char_width(text_area)) |
164 (text_area.offsetToXY(stop - 1), char_width(text_area)) |
171 else (text_area.offsetToXY(stop), 0) |
165 else (text_area.offsetToXY(stop), 0) |
172 |
166 |
173 if (p != null && q != null && p.x < q.x + r && p.y == q.y) |
167 if (p != null && q != null && p.x < q.x + r && p.y == q.y) |