author | wenzelm |
Tue, 14 Jun 2011 12:18:34 +0200 | |
changeset 43382 | 5d9d34bdec25 |
parent 43381 | 806878ae2219 |
child 43383 | 63fc6b5ef8ac |
permissions | -rw-r--r-- |
43381 | 1 |
/* Title: Tools/jEdit/src/text_area_painter.scala |
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
3 |
|
43381 | 4 |
Painter setup for main jEdit text area. |
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
6 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle.jedit |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
8 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
9 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
10 |
import isabelle._ |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
11 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
12 |
import java.awt.{Graphics, Graphics2D} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
13 |
import java.util.ArrayList |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
14 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
15 |
import org.gjt.sp.jedit.Debug |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
16 |
import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
17 |
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
18 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
19 |
|
43381 | 20 |
class Text_Area_Painter(doc_view: Document_View) |
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
21 |
{ |
43381 | 22 |
private val model = doc_view.model |
43382 | 23 |
private val buffer = model.buffer |
43376
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
24 |
private val text_area = doc_view.text_area |
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
25 |
|
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
26 |
private val orig_text_painter: TextAreaExtension = |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
27 |
{ |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
28 |
val name = "org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText" |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
29 |
text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
30 |
match { |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
31 |
case List(x) => x |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
32 |
case _ => error("Expected exactly one " + name) |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
33 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
34 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
35 |
|
43381 | 36 |
|
37 |
/* painter snapshot */ |
|
38 |
||
39 |
@volatile private var _painter_snapshot: Option[Document.Snapshot] = None |
|
40 |
||
41 |
private def painter_snapshot(): Document.Snapshot = |
|
42 |
_painter_snapshot match { |
|
43 |
case Some(snapshot) => snapshot |
|
44 |
case None => error("Missing document snapshot for text area painter") |
|
45 |
} |
|
46 |
||
47 |
private val set_snapshot = new TextAreaExtension |
|
48 |
{ |
|
49 |
override def paintScreenLineRange(gfx: Graphics2D, |
|
50 |
first_line: Int, last_line: Int, physical_lines: Array[Int], |
|
51 |
start: Array[Int], end: Array[Int], y: Int, line_height: Int) |
|
52 |
{ |
|
53 |
_painter_snapshot = Some(model.snapshot()) |
|
54 |
} |
|
55 |
} |
|
56 |
||
57 |
private val reset_snapshot = new TextAreaExtension |
|
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
58 |
{ |
43381 | 59 |
override def paintScreenLineRange(gfx: Graphics2D, |
60 |
first_line: Int, last_line: Int, physical_lines: Array[Int], |
|
61 |
start: Array[Int], end: Array[Int], y: Int, line_height: Int) |
|
62 |
{ |
|
63 |
_painter_snapshot = None |
|
64 |
} |
|
65 |
} |
|
66 |
||
67 |
||
68 |
/* text background */ |
|
43376
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
69 |
|
43381 | 70 |
private val background_painter = new TextAreaExtension |
71 |
{ |
|
72 |
override def paintScreenLineRange(gfx: Graphics2D, |
|
73 |
first_line: Int, last_line: Int, physical_lines: Array[Int], |
|
74 |
start: Array[Int], end: Array[Int], y: Int, line_height: Int) |
|
75 |
{ |
|
43382 | 76 |
Isabelle.swing_buffer_lock(buffer) { |
43381 | 77 |
val snapshot = painter_snapshot() |
78 |
val ascent = text_area.getPainter.getFontMetrics.getAscent |
|
43376
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
79 |
|
43381 | 80 |
for (i <- 0 until physical_lines.length) { |
81 |
if (physical_lines(i) != -1) { |
|
82 |
val line_range = doc_view.proper_line_range(start(i), end(i)) |
|
43376
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
83 |
|
43381 | 84 |
// background color: status |
85 |
val cmds = snapshot.node.command_range(snapshot.revert(line_range)) |
|
86 |
for { |
|
87 |
(command, command_start) <- cmds if !command.is_ignored |
|
88 |
val range = line_range.restrict(snapshot.convert(command.range + command_start)) |
|
89 |
r <- Isabelle.gfx_range(text_area, range) |
|
90 |
color <- Isabelle_Markup.status_color(snapshot, command) |
|
91 |
} { |
|
92 |
gfx.setColor(color) |
|
93 |
gfx.fillRect(r.x, y + i * line_height, r.length, line_height) |
|
94 |
} |
|
43376
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
95 |
|
43381 | 96 |
// background color (1): markup |
97 |
for { |
|
98 |
Text.Info(range, Some(color)) <- |
|
99 |
snapshot.select_markup(line_range)(Isabelle_Markup.background1).iterator |
|
100 |
r <- Isabelle.gfx_range(text_area, range) |
|
101 |
} { |
|
102 |
gfx.setColor(color) |
|
103 |
gfx.fillRect(r.x, y + i * line_height, r.length, line_height) |
|
104 |
} |
|
43376
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
105 |
|
43381 | 106 |
// background color (2): markup |
107 |
for { |
|
108 |
Text.Info(range, Some(color)) <- |
|
109 |
snapshot.select_markup(line_range)(Isabelle_Markup.background2).iterator |
|
110 |
r <- Isabelle.gfx_range(text_area, range) |
|
111 |
} { |
|
112 |
gfx.setColor(color) |
|
113 |
gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4) |
|
43376
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
114 |
} |
43381 | 115 |
|
116 |
// sub-expression highlighting -- potentially from other snapshot |
|
117 |
doc_view.highlight_range match { |
|
118 |
case Some((range, color)) if line_range.overlaps(range) => |
|
119 |
Isabelle.gfx_range(text_area, line_range.restrict(range)) match { |
|
120 |
case None => |
|
121 |
case Some(r) => |
|
122 |
gfx.setColor(color) |
|
123 |
gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1) |
|
124 |
} |
|
125 |
case _ => |
|
126 |
} |
|
127 |
||
128 |
// squiggly underline |
|
129 |
for { |
|
130 |
Text.Info(range, Some(color)) <- |
|
131 |
snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator |
|
132 |
r <- Isabelle.gfx_range(text_area, range) |
|
133 |
} { |
|
134 |
gfx.setColor(color) |
|
135 |
val x0 = (r.x / 2) * 2 |
|
136 |
val y0 = r.y + ascent + 1 |
|
137 |
for (x1 <- Range(x0, x0 + r.length, 2)) { |
|
138 |
val y1 = if (x1 % 4 < 2) y0 else y0 + 1 |
|
139 |
gfx.drawLine(x1, y1, x1 + 1, y1) |
|
43376
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
140 |
} |
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
141 |
} |
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
142 |
} |
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
143 |
} |
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
144 |
} |
43381 | 145 |
} |
146 |
} |
|
147 |
||
148 |
||
149 |
/* text */ |
|
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
150 |
|
43382 | 151 |
private def line_infos(physical_lines: Iterator[Int]): Map[Text.Offset, Chunk] = |
152 |
{ |
|
153 |
val painter = text_area.getPainter |
|
154 |
val font = painter.getFont |
|
155 |
val font_context = painter.getFontRenderContext |
|
156 |
||
157 |
// see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged |
|
158 |
// see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength |
|
159 |
val margin = |
|
160 |
if (buffer.getStringProperty("wrap") != "soft") 0.0f |
|
161 |
else { |
|
162 |
val max = buffer.getIntegerProperty("maxLineLen", 0) |
|
163 |
if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt |
|
164 |
else painter.getWidth - font.getStringBounds(" ", font_context).getWidth.round.toInt * 3 |
|
165 |
}.toFloat |
|
166 |
||
167 |
val out = new ArrayList[Chunk] |
|
168 |
val handler = new DisplayTokenHandler |
|
169 |
||
170 |
var result = Map[Text.Offset, Chunk]() |
|
171 |
for (line <- physical_lines) { |
|
172 |
out.clear |
|
173 |
handler.init(painter.getStyles, font_context, painter, out, margin) |
|
174 |
buffer.markTokens(line, handler) |
|
175 |
||
176 |
val line_start = buffer.getLineStartOffset(line) |
|
177 |
for (i <- 0 until out.size) { |
|
178 |
val chunk = out.get(i) |
|
179 |
result += (line_start + chunk.offset -> chunk) |
|
180 |
} |
|
181 |
} |
|
182 |
result |
|
183 |
} |
|
184 |
||
185 |
private def paint_chunk_list(gfx: Graphics2D, |
|
186 |
offset: Text.Offset, head: Chunk, x: Float, y: Float): Float = |
|
187 |
{ |
|
188 |
val clip_rect = gfx.getClipBounds |
|
189 |
val font_context = text_area.getPainter.getFontRenderContext |
|
190 |
||
191 |
var w = 0.0f |
|
192 |
var chunk_offset = offset |
|
193 |
var chunk = head |
|
194 |
while (chunk != null) { |
|
195 |
val chunk_length = if (chunk.str == null) 0 else chunk.str.length |
|
196 |
||
197 |
if (x + w + chunk.width > clip_rect.x && |
|
198 |
x + w < clip_rect.x + clip_rect.width && |
|
199 |
chunk.accessable && chunk.visible) |
|
200 |
{ |
|
201 |
val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk_length) |
|
202 |
val chunk_font = chunk.style.getFont |
|
203 |
val chunk_color = chunk.style.getForegroundColor |
|
204 |
||
205 |
val markup = painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground) |
|
206 |
||
207 |
gfx.setFont(chunk_font) |
|
208 |
if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null && |
|
209 |
markup.forall(info => info.info.isEmpty)) { |
|
210 |
gfx.setColor(chunk_color) |
|
211 |
gfx.drawGlyphVector(chunk.gv, x + w, y) |
|
212 |
} |
|
213 |
else { |
|
214 |
var xpos = x + w |
|
215 |
for (Text.Info(range, info) <- markup) { |
|
216 |
val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset) |
|
217 |
gfx.setColor(info.getOrElse(chunk_color)) |
|
218 |
gfx.drawString(str, xpos.toInt, y.toInt) |
|
219 |
xpos += chunk_font.getStringBounds(str, font_context).getWidth.toFloat |
|
220 |
} |
|
221 |
} |
|
222 |
} |
|
223 |
w += chunk.width |
|
224 |
chunk_offset += chunk_length |
|
225 |
chunk = chunk.next.asInstanceOf[Chunk] |
|
226 |
} |
|
227 |
w |
|
228 |
} |
|
229 |
||
43381 | 230 |
private val text_painter = new TextAreaExtension |
231 |
{ |
|
232 |
override def paintScreenLineRange(gfx: Graphics2D, |
|
233 |
first_line: Int, last_line: Int, physical_lines: Array[Int], |
|
43382 | 234 |
start: Array[Int], end: Array[Int], y: Int, line_height: Int) |
43381 | 235 |
{ |
236 |
Isabelle.swing_buffer_lock(buffer) { |
|
237 |
val clip = gfx.getClip |
|
238 |
val x0 = text_area.getHorizontalOffset |
|
43382 | 239 |
val fm = text_area.getPainter.getFontMetrics |
240 |
var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent |
|
43372
2df2144b0910
use orig_text_painter for extras outside main text (also required to update internal line infos);
wenzelm
parents:
43371
diff
changeset
|
241 |
|
43382 | 242 |
val infos = line_infos(physical_lines.iterator.filter(i => i != -1)) |
43381 | 243 |
for (i <- 0 until physical_lines.length) { |
244 |
if (physical_lines(i) != -1) { |
|
43382 | 245 |
infos.get(start(i)) match { |
43381 | 246 |
case Some(chunk) => |
43382 | 247 |
val w = paint_chunk_list(gfx, start(i), chunk, x0, y0).toInt |
43381 | 248 |
gfx.clipRect(x0 + w, 0, Integer.MAX_VALUE, Integer.MAX_VALUE) |
249 |
orig_text_painter.paintValidLine(gfx, |
|
43382 | 250 |
first_line + i, physical_lines(i), start(i), end(i), y + line_height * i) |
43381 | 251 |
gfx.setClip(clip) |
252 |
case None => |
|
253 |
} |
|
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
254 |
} |
43381 | 255 |
y0 += line_height |
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
256 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
257 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
258 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
259 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
260 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
261 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
262 |
/* activation */ |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
263 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
264 |
def activate() |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
265 |
{ |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
266 |
val painter = text_area.getPainter |
43381 | 267 |
painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_snapshot) |
268 |
painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter) |
|
269 |
painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter) |
|
270 |
painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_snapshot) |
|
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
271 |
painter.removeExtension(orig_text_painter) |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
272 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
273 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
274 |
def deactivate() |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
275 |
{ |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
276 |
val painter = text_area.getPainter |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
277 |
painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter) |
43381 | 278 |
painter.removeExtension(reset_snapshot) |
279 |
painter.removeExtension(text_painter) |
|
280 |
painter.removeExtension(background_painter) |
|
281 |
painter.removeExtension(set_snapshot) |
|
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
282 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
283 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
284 |