105 val buffer = text_area.getBuffer |
105 val buffer = text_area.getBuffer |
106 text_area.invalidateLineRange( |
106 text_area.invalidateLineRange( |
107 buffer.getLineOfOffset(range.start), |
107 buffer.getLineOfOffset(range.start), |
108 buffer.getLineOfOffset(range.stop)) |
108 buffer.getLineOfOffset(range.stop)) |
109 } |
109 } |
|
110 |
|
111 |
|
112 /* char width */ |
|
113 |
|
114 def char_width(text_area: TextArea): Int = |
|
115 { |
|
116 val painter = text_area.getPainter |
|
117 val font = painter.getFont |
|
118 val font_context = painter.getFontRenderContext |
|
119 font.getStringBounds(" ", font_context).getWidth.round.toInt |
|
120 } |
|
121 |
|
122 |
|
123 /* graphics range */ |
|
124 |
|
125 class Gfx_Range(val x: Int, val y: Int, val length: Int) |
|
126 |
|
127 // NB: jEdit already normalizes \r\n and \r to \n |
|
128 // NB: last line lacks \n |
|
129 def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] = |
|
130 { |
|
131 val buffer = text_area.getBuffer |
|
132 |
|
133 val p = text_area.offsetToXY(range.start) |
|
134 |
|
135 val end = buffer.getLength |
|
136 val stop = range.stop |
|
137 val (q, r) = |
|
138 if (stop >= end) (text_area.offsetToXY(end), char_width(text_area)) |
|
139 else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n") |
|
140 (text_area.offsetToXY(stop - 1), char_width(text_area)) |
|
141 else (text_area.offsetToXY(stop), 0) |
|
142 |
|
143 if (p != null && q != null && p.x < q.x + r && p.y == q.y) |
|
144 Some(new Gfx_Range(p.x, p.y, q.x + r - p.x)) |
|
145 else None |
|
146 } |
110 } |
147 } |
111 |
148 |