8 |
8 |
9 |
9 |
10 import isabelle._ |
10 import isabelle._ |
11 |
11 |
12 import java.awt.Graphics2D |
12 import java.awt.Graphics2D |
|
13 import java.awt.font.TextAttribute |
|
14 import java.text.AttributedString |
13 import java.util.ArrayList |
15 import java.util.ArrayList |
14 |
16 |
15 import org.gjt.sp.jedit.Debug |
17 import org.gjt.sp.jedit.Debug |
16 import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk} |
18 import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk} |
17 import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter} |
19 import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, JEditTextArea} |
18 |
20 |
19 |
21 |
20 class Text_Area_Painter(doc_view: Document_View) |
22 class Text_Area_Painter(doc_view: Document_View) |
21 { |
23 { |
22 private val model = doc_view.model |
24 private val model = doc_view.model |
23 private val buffer = model.buffer |
25 private val buffer = model.buffer |
24 private val text_area = doc_view.text_area |
26 private val text_area = doc_view.text_area |
25 |
27 |
26 private val orig_text_painter: TextAreaExtension = |
28 |
27 { |
29 /* original painters */ |
28 val name = "org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText" |
30 |
|
31 private def pick_extension(name: String): TextAreaExtension = |
|
32 { |
29 text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList |
33 text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList |
30 match { |
34 match { |
31 case List(x) => x |
35 case List(x) => x |
32 case _ => error("Expected exactly one " + name) |
36 case _ => error("Expected exactly one " + name) |
33 } |
37 } |
34 } |
38 } |
|
39 |
|
40 private val orig_text_painter = |
|
41 pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText") |
|
42 |
|
43 private val orig_caret_painter = |
|
44 pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintCaret") |
35 |
45 |
36 |
46 |
37 /* painter snapshot */ |
47 /* painter snapshot */ |
38 |
48 |
39 @volatile private var _painter_snapshot: Option[Document.Snapshot] = None |
49 @volatile private var _painter_snapshot: Option[Document.Snapshot] = None |
181 } |
191 } |
182 result |
192 result |
183 } |
193 } |
184 |
194 |
185 private def paint_chunk_list(gfx: Graphics2D, |
195 private def paint_chunk_list(gfx: Graphics2D, |
186 offset: Text.Offset, head: Chunk, x: Float, y: Float): Float = |
196 offset: Text.Offset, caret_offset: Text.Offset, head: Chunk, x: Float, y: Float): Float = |
187 { |
197 { |
188 val clip_rect = gfx.getClipBounds |
198 val clip_rect = gfx.getClipBounds |
189 val font_context = text_area.getPainter.getFontRenderContext |
199 val painter = text_area.getPainter |
|
200 val font_context = painter.getFontRenderContext |
190 |
201 |
191 var w = 0.0f |
202 var w = 0.0f |
192 var chunk_offset = offset |
203 var chunk_offset = offset |
193 var chunk = head |
204 var chunk = head |
194 while (chunk != null) { |
205 while (chunk != null) { |
204 |
215 |
205 val markup = painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground) |
216 val markup = painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground) |
206 |
217 |
207 gfx.setFont(chunk_font) |
218 gfx.setFont(chunk_font) |
208 if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null && |
219 if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null && |
209 markup.forall(info => info.info.isEmpty)) { |
220 markup.forall(info => info.info.isEmpty) && |
|
221 !chunk_range.contains(caret_offset)) { |
210 gfx.setColor(chunk_color) |
222 gfx.setColor(chunk_color) |
211 gfx.drawGlyphVector(chunk.gv, x + w, y) |
223 gfx.drawGlyphVector(chunk.gv, x + w, y) |
212 } |
224 } |
213 else { |
225 else { |
214 var x1 = x + w |
226 var x1 = x + w |
215 for (Text.Info(range, info) <- markup) { |
227 for (Text.Info(range, info) <- markup) { |
216 val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset) |
228 val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset) |
217 gfx.setColor(info.getOrElse(chunk_color)) |
229 gfx.setColor(info.getOrElse(chunk_color)) |
218 gfx.drawString(str, x1.toInt, y.toInt) |
230 if (range.contains(caret_offset)) { |
|
231 val astr = new AttributedString(str) |
|
232 val i = caret_offset - range.start |
|
233 astr.addAttribute(TextAttribute.FONT, chunk_font) |
|
234 astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, i + 1) |
|
235 astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, i + 1) |
|
236 gfx.drawString(astr.getIterator, x1.toInt, y.toInt) |
|
237 } |
|
238 else { |
|
239 gfx.drawString(str, x1.toInt, y.toInt) |
|
240 } |
219 x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat |
241 x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat |
220 } |
242 } |
221 } |
243 } |
222 } |
244 } |
223 w += chunk.width |
245 w += chunk.width |
237 val clip = gfx.getClip |
259 val clip = gfx.getClip |
238 val x0 = text_area.getHorizontalOffset |
260 val x0 = text_area.getHorizontalOffset |
239 val fm = text_area.getPainter.getFontMetrics |
261 val fm = text_area.getPainter.getFontMetrics |
240 var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent |
262 var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent |
241 |
263 |
|
264 val caret_offset = |
|
265 if (text_area.hasFocus) text_area.getCaretPosition |
|
266 else -1 |
|
267 |
242 val infos = line_infos(physical_lines.iterator.filter(i => i != -1)) |
268 val infos = line_infos(physical_lines.iterator.filter(i => i != -1)) |
243 for (i <- 0 until physical_lines.length) { |
269 for (i <- 0 until physical_lines.length) { |
244 if (physical_lines(i) != -1) { |
270 if (physical_lines(i) != -1) { |
245 infos.get(start(i)) match { |
271 val x1 = |
246 case Some(chunk) => |
272 infos.get(start(i)) match { |
247 val w = paint_chunk_list(gfx, start(i), chunk, x0, y0).toInt |
273 case None => x0 |
248 gfx.clipRect(x0 + w, 0, Integer.MAX_VALUE, Integer.MAX_VALUE) |
274 case Some(chunk) => |
249 orig_text_painter.paintValidLine(gfx, |
275 gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height) |
250 first_line + i, physical_lines(i), start(i), end(i), y + line_height * i) |
276 val w = paint_chunk_list(gfx, start(i), caret_offset, chunk, x0, y0).toInt |
251 gfx.setClip(clip) |
277 x0 + w.toInt |
252 case None => |
278 } |
253 } |
279 gfx.clipRect(x1, 0, Integer.MAX_VALUE, Integer.MAX_VALUE) |
|
280 orig_text_painter.paintValidLine(gfx, |
|
281 first_line + i, physical_lines(i), start(i), end(i), y + line_height * i) |
|
282 orig_caret_painter.paintValidLine(gfx, |
|
283 first_line + i, physical_lines(i), start(i), end(i), y + line_height * i) |
|
284 gfx.setClip(clip) |
254 } |
285 } |
255 y0 += line_height |
286 y0 += line_height |
256 } |
287 } |
257 } |
288 } |
258 } |
289 } |
267 painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_snapshot) |
298 painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_snapshot) |
268 painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter) |
299 painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter) |
269 painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter) |
300 painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter) |
270 painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_snapshot) |
301 painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_snapshot) |
271 painter.removeExtension(orig_text_painter) |
302 painter.removeExtension(orig_text_painter) |
|
303 painter.removeExtension(orig_caret_painter) |
272 } |
304 } |
273 |
305 |
274 def deactivate() |
306 def deactivate() |
275 { |
307 { |
276 val painter = text_area.getPainter |
308 val painter = text_area.getPainter |
|
309 val caret_layer = |
|
310 if (painter.isBlockCaretEnabled) TextAreaPainter.BLOCK_CARET_LAYER |
|
311 else TextAreaPainter.CARET_LAYER |
|
312 painter.addExtension(caret_layer, orig_caret_painter) |
277 painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter) |
313 painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter) |
278 painter.removeExtension(reset_snapshot) |
314 painter.removeExtension(reset_snapshot) |
279 painter.removeExtension(text_painter) |
315 painter.removeExtension(text_painter) |
280 painter.removeExtension(background_painter) |
316 painter.removeExtension(background_painter) |
281 painter.removeExtension(set_snapshot) |
317 painter.removeExtension(set_snapshot) |