author | wenzelm |
Sun, 04 Mar 2012 23:04:40 +0100 | |
changeset 46817 | 90c8620852cf |
parent 46812 | 3d55ef732cd7 |
child 46913 | 3444a24dc4e9 |
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 |
|
46220
663251a395c2
more explicit/robust treatment of common snapshot;
wenzelm
parents:
46205
diff
changeset
|
4 |
Painter setup for main jEdit text area, depending on common snapshot. |
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 |
|
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
12 |
import java.awt.{Graphics2D, Shape} |
43392 | 13 |
import java.awt.font.TextAttribute |
14 |
import java.text.AttributedString |
|
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
15 |
import java.util.ArrayList |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
16 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
17 |
import org.gjt.sp.jedit.Debug |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
18 |
import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk} |
46224 | 19 |
import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter} |
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
20 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
21 |
|
43381 | 22 |
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
|
23 |
{ |
43381 | 24 |
private val model = doc_view.model |
43382 | 25 |
private val buffer = model.buffer |
43376
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
26 |
private val text_area = doc_view.text_area |
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
27 |
|
43392 | 28 |
|
46220
663251a395c2
more explicit/robust treatment of common snapshot;
wenzelm
parents:
46205
diff
changeset
|
29 |
/* graphics range */ |
46204 | 30 |
|
46812
3d55ef732cd7
clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
wenzelm
parents:
46224
diff
changeset
|
31 |
private def char_width(): Int = |
3d55ef732cd7
clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
wenzelm
parents:
46224
diff
changeset
|
32 |
{ |
3d55ef732cd7
clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
wenzelm
parents:
46224
diff
changeset
|
33 |
val painter = text_area.getPainter |
3d55ef732cd7
clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
wenzelm
parents:
46224
diff
changeset
|
34 |
val font = painter.getFont |
3d55ef732cd7
clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
wenzelm
parents:
46224
diff
changeset
|
35 |
val font_context = painter.getFontRenderContext |
3d55ef732cd7
clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
wenzelm
parents:
46224
diff
changeset
|
36 |
font.getStringBounds(" ", font_context).getWidth.round.toInt |
3d55ef732cd7
clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
wenzelm
parents:
46224
diff
changeset
|
37 |
} |
3d55ef732cd7
clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
wenzelm
parents:
46224
diff
changeset
|
38 |
|
46204 | 39 |
private class Gfx_Range(val x: Int, val y: Int, val length: Int) |
40 |
||
46812
3d55ef732cd7
clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
wenzelm
parents:
46224
diff
changeset
|
41 |
// NB: jEdit already normalizes \r\n and \r to \n |
3d55ef732cd7
clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
wenzelm
parents:
46224
diff
changeset
|
42 |
// NB: last line lacks \n |
46204 | 43 |
private def gfx_range(range: Text.Range): Option[Gfx_Range] = |
44 |
{ |
|
45 |
val p = text_area.offsetToXY(range.start) |
|
46812
3d55ef732cd7
clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
wenzelm
parents:
46224
diff
changeset
|
46 |
|
3d55ef732cd7
clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
wenzelm
parents:
46224
diff
changeset
|
47 |
val end = buffer.getLength |
3d55ef732cd7
clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
wenzelm
parents:
46224
diff
changeset
|
48 |
val stop = range.stop |
3d55ef732cd7
clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
wenzelm
parents:
46224
diff
changeset
|
49 |
val (q, r) = |
3d55ef732cd7
clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
wenzelm
parents:
46224
diff
changeset
|
50 |
if (stop >= end) (text_area.offsetToXY(end), char_width()) |
3d55ef732cd7
clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
wenzelm
parents:
46224
diff
changeset
|
51 |
else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n") |
3d55ef732cd7
clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
wenzelm
parents:
46224
diff
changeset
|
52 |
(text_area.offsetToXY(stop - 1), char_width()) |
3d55ef732cd7
clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
wenzelm
parents:
46224
diff
changeset
|
53 |
else (text_area.offsetToXY(stop), 0) |
3d55ef732cd7
clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
wenzelm
parents:
46224
diff
changeset
|
54 |
|
3d55ef732cd7
clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
wenzelm
parents:
46224
diff
changeset
|
55 |
if (p != null && q != null && p.x < q.x + r && p.y == q.y) |
3d55ef732cd7
clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
wenzelm
parents:
46224
diff
changeset
|
56 |
Some(new Gfx_Range(p.x, p.y, q.x + r - p.x)) |
46204 | 57 |
else None |
58 |
} |
|
59 |
||
60 |
||
43392 | 61 |
/* original painters */ |
62 |
||
63 |
private def pick_extension(name: String): TextAreaExtension = |
|
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
64 |
{ |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
65 |
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
|
66 |
match { |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
67 |
case List(x) => x |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
68 |
case _ => error("Expected exactly one " + name) |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
69 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
70 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
71 |
|
43392 | 72 |
private val orig_text_painter = |
73 |
pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText") |
|
74 |
||
75 |
||
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
76 |
/* common painter state */ |
43381 | 77 |
|
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
78 |
@volatile private var painter_snapshot: Document.Snapshot = null |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
79 |
@volatile private var painter_clip: Shape = null |
43381 | 80 |
|
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
81 |
private val set_state = new TextAreaExtension |
43381 | 82 |
{ |
83 |
override def paintScreenLineRange(gfx: Graphics2D, |
|
84 |
first_line: Int, last_line: Int, physical_lines: Array[Int], |
|
85 |
start: Array[Int], end: Array[Int], y: Int, line_height: Int) |
|
86 |
{ |
|
46220
663251a395c2
more explicit/robust treatment of common snapshot;
wenzelm
parents:
46205
diff
changeset
|
87 |
painter_snapshot = doc_view.update_snapshot() |
663251a395c2
more explicit/robust treatment of common snapshot;
wenzelm
parents:
46205
diff
changeset
|
88 |
painter_clip = gfx.getClip |
43381 | 89 |
} |
90 |
} |
|
91 |
||
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
92 |
private val reset_state = new TextAreaExtension |
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
93 |
{ |
43381 | 94 |
override def paintScreenLineRange(gfx: Graphics2D, |
95 |
first_line: Int, last_line: Int, physical_lines: Array[Int], |
|
96 |
start: Array[Int], end: Array[Int], y: Int, line_height: Int) |
|
97 |
{ |
|
46220
663251a395c2
more explicit/robust treatment of common snapshot;
wenzelm
parents:
46205
diff
changeset
|
98 |
painter_snapshot = null |
663251a395c2
more explicit/robust treatment of common snapshot;
wenzelm
parents:
46205
diff
changeset
|
99 |
painter_clip = null |
43381 | 100 |
} |
101 |
} |
|
102 |
||
46220
663251a395c2
more explicit/robust treatment of common snapshot;
wenzelm
parents:
46205
diff
changeset
|
103 |
private def robust_snapshot(body: Document.Snapshot => Unit) |
663251a395c2
more explicit/robust treatment of common snapshot;
wenzelm
parents:
46205
diff
changeset
|
104 |
{ |
663251a395c2
more explicit/robust treatment of common snapshot;
wenzelm
parents:
46205
diff
changeset
|
105 |
doc_view.robust_body(()) { body(painter_snapshot) } |
663251a395c2
more explicit/robust treatment of common snapshot;
wenzelm
parents:
46205
diff
changeset
|
106 |
} |
663251a395c2
more explicit/robust treatment of common snapshot;
wenzelm
parents:
46205
diff
changeset
|
107 |
|
43381 | 108 |
|
109 |
/* text background */ |
|
43376
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
110 |
|
43381 | 111 |
private val background_painter = new TextAreaExtension |
112 |
{ |
|
113 |
override def paintScreenLineRange(gfx: Graphics2D, |
|
114 |
first_line: Int, last_line: Int, physical_lines: Array[Int], |
|
115 |
start: Array[Int], end: Array[Int], y: Int, line_height: Int) |
|
116 |
{ |
|
46220
663251a395c2
more explicit/robust treatment of common snapshot;
wenzelm
parents:
46205
diff
changeset
|
117 |
robust_snapshot { snapshot => |
43381 | 118 |
val ascent = text_area.getPainter.getFontMetrics.getAscent |
43376
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
119 |
|
43381 | 120 |
for (i <- 0 until physical_lines.length) { |
121 |
if (physical_lines(i) != -1) { |
|
122 |
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
|
123 |
|
46166 | 124 |
// background color (1) |
43381 | 125 |
for { |
46178
1c5c88f6feb5
clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents:
46166
diff
changeset
|
126 |
Text.Info(range, color) <- Isabelle_Rendering.background1(snapshot, line_range) |
46204 | 127 |
r <- gfx_range(range) |
43381 | 128 |
} { |
129 |
gfx.setColor(color) |
|
130 |
gfx.fillRect(r.x, y + i * line_height, r.length, line_height) |
|
131 |
} |
|
43376
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
132 |
|
46166 | 133 |
// background color (2) |
43381 | 134 |
for { |
46178
1c5c88f6feb5
clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents:
46166
diff
changeset
|
135 |
Text.Info(range, color) <- Isabelle_Rendering.background2(snapshot, line_range) |
46204 | 136 |
r <- gfx_range(range) |
43381 | 137 |
} { |
138 |
gfx.setColor(color) |
|
139 |
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
|
140 |
} |
43381 | 141 |
|
142 |
// squiggly underline |
|
143 |
for { |
|
46224 | 144 |
Text.Info(range, color) <- Isabelle_Rendering.squiggly_underline(snapshot, line_range) |
46204 | 145 |
r <- gfx_range(range) |
43381 | 146 |
} { |
147 |
gfx.setColor(color) |
|
148 |
val x0 = (r.x / 2) * 2 |
|
149 |
val y0 = r.y + ascent + 1 |
|
150 |
for (x1 <- Range(x0, x0 + r.length, 2)) { |
|
151 |
val y1 = if (x1 % 4 < 2) y0 else y0 + 1 |
|
152 |
gfx.drawLine(x1, y1, x1 + 1, y1) |
|
43376
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
153 |
} |
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
154 |
} |
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
155 |
} |
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
156 |
} |
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
157 |
} |
43381 | 158 |
} |
159 |
} |
|
160 |
||
161 |
||
162 |
/* text */ |
|
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
163 |
|
43382 | 164 |
private def line_infos(physical_lines: Iterator[Int]): Map[Text.Offset, Chunk] = |
165 |
{ |
|
166 |
val painter = text_area.getPainter |
|
167 |
val font = painter.getFont |
|
168 |
val font_context = painter.getFontRenderContext |
|
169 |
||
170 |
// see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged |
|
171 |
// see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength |
|
172 |
val margin = |
|
173 |
if (buffer.getStringProperty("wrap") != "soft") 0.0f |
|
174 |
else { |
|
175 |
val max = buffer.getIntegerProperty("maxLineLen", 0) |
|
176 |
if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt |
|
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
177 |
else painter.getWidth - char_width() * 3 |
43382 | 178 |
}.toFloat |
179 |
||
180 |
val out = new ArrayList[Chunk] |
|
181 |
val handler = new DisplayTokenHandler |
|
182 |
||
183 |
var result = Map[Text.Offset, Chunk]() |
|
184 |
for (line <- physical_lines) { |
|
46817 | 185 |
val line_start = buffer.getLineStartOffset(line) |
186 |
||
43382 | 187 |
out.clear |
46817 | 188 |
handler.init(painter.getStyles, font_context, painter, out, margin) // jedit-4.5.0: line_start |
43382 | 189 |
buffer.markTokens(line, handler) |
190 |
||
191 |
for (i <- 0 until out.size) { |
|
192 |
val chunk = out.get(i) |
|
193 |
result += (line_start + chunk.offset -> chunk) |
|
194 |
} |
|
195 |
} |
|
196 |
result |
|
197 |
} |
|
198 |
||
46220
663251a395c2
more explicit/robust treatment of common snapshot;
wenzelm
parents:
46205
diff
changeset
|
199 |
private def paint_chunk_list(snapshot: Document.Snapshot, |
43505 | 200 |
gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float = |
43382 | 201 |
{ |
202 |
val clip_rect = gfx.getClipBounds |
|
43392 | 203 |
val painter = text_area.getPainter |
204 |
val font_context = painter.getFontRenderContext |
|
43382 | 205 |
|
206 |
var w = 0.0f |
|
207 |
var chunk = head |
|
208 |
while (chunk != null) { |
|
43505 | 209 |
val chunk_offset = line_start + chunk.offset |
43382 | 210 |
if (x + w + chunk.width > clip_rect.x && |
43506 | 211 |
x + w < clip_rect.x + clip_rect.width && chunk.accessable) |
43382 | 212 |
{ |
43505 | 213 |
val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length) |
44662
c8f1d943bfc5
more robust chunk painting wrt. hard tabs, when chunk.str == null;
wenzelm
parents:
44545
diff
changeset
|
214 |
val chunk_str = if (chunk.str == null) " " * chunk.length else chunk.str |
43382 | 215 |
val chunk_font = chunk.style.getFont |
216 |
val chunk_color = chunk.style.getForegroundColor |
|
217 |
||
44056
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
218 |
def string_width(s: String): Float = |
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
219 |
if (s.isEmpty) 0.0f |
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
220 |
else chunk_font.getStringBounds(s, font_context).getWidth.toFloat |
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
221 |
|
43448
90aec5043461
more robust caret painting wrt. surrogate characters;
wenzelm
parents:
43435
diff
changeset
|
222 |
val caret_range = |
90aec5043461
more robust caret painting wrt. surrogate characters;
wenzelm
parents:
43435
diff
changeset
|
223 |
if (text_area.hasFocus) doc_view.caret_range() |
90aec5043461
more robust caret painting wrt. surrogate characters;
wenzelm
parents:
43435
diff
changeset
|
224 |
else Text.Range(-1) |
90aec5043461
more robust caret painting wrt. surrogate characters;
wenzelm
parents:
43435
diff
changeset
|
225 |
|
43426
24e2e2f0032b
more explicit treatment of ranges after revert/convert, which may well distort the overall start/end positions;
wenzelm
parents:
43419
diff
changeset
|
226 |
val markup = |
43428
b41dea5772c6
more robust treatment of partial range restriction;
wenzelm
parents:
43426
diff
changeset
|
227 |
for { |
46220
663251a395c2
more explicit/robust treatment of common snapshot;
wenzelm
parents:
46205
diff
changeset
|
228 |
r1 <- Isabelle_Rendering.text_color(snapshot, chunk_range, chunk_color) |
43450 | 229 |
r2 <- r1.try_restrict(chunk_range) |
230 |
} yield r2 |
|
43382 | 231 |
|
43759
d93a69672362
more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents:
43506
diff
changeset
|
232 |
val padded_markup = |
d93a69672362
more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents:
43506
diff
changeset
|
233 |
if (markup.isEmpty) |
46197
e4da482283ef
tuned text_color: cumulate with explicit default color;
wenzelm
parents:
46178
diff
changeset
|
234 |
Iterator(Text.Info(chunk_range, chunk_color)) |
43759
d93a69672362
more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents:
43506
diff
changeset
|
235 |
else |
46197
e4da482283ef
tuned text_color: cumulate with explicit default color;
wenzelm
parents:
46178
diff
changeset
|
236 |
Iterator( |
e4da482283ef
tuned text_color: cumulate with explicit default color;
wenzelm
parents:
46178
diff
changeset
|
237 |
Text.Info(Text.Range(chunk_range.start, markup.head.range.start), chunk_color)) ++ |
43759
d93a69672362
more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents:
43506
diff
changeset
|
238 |
markup.iterator ++ |
46197
e4da482283ef
tuned text_color: cumulate with explicit default color;
wenzelm
parents:
46178
diff
changeset
|
239 |
Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), chunk_color)) |
43759
d93a69672362
more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents:
43506
diff
changeset
|
240 |
|
43450 | 241 |
var x1 = x + w |
43382 | 242 |
gfx.setFont(chunk_font) |
46197
e4da482283ef
tuned text_color: cumulate with explicit default color;
wenzelm
parents:
46178
diff
changeset
|
243 |
for (Text.Info(range, color) <- padded_markup if !range.is_singularity) { |
44662
c8f1d943bfc5
more robust chunk painting wrt. hard tabs, when chunk.str == null;
wenzelm
parents:
44545
diff
changeset
|
244 |
val str = chunk_str.substring(range.start - chunk_offset, range.stop - chunk_offset) |
46197
e4da482283ef
tuned text_color: cumulate with explicit default color;
wenzelm
parents:
46178
diff
changeset
|
245 |
gfx.setColor(color) |
43448
90aec5043461
more robust caret painting wrt. surrogate characters;
wenzelm
parents:
43435
diff
changeset
|
246 |
|
43759
d93a69672362
more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents:
43506
diff
changeset
|
247 |
range.try_restrict(caret_range) match { |
d93a69672362
more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents:
43506
diff
changeset
|
248 |
case Some(r) if !r.is_singularity => |
d93a69672362
more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents:
43506
diff
changeset
|
249 |
val i = r.start - range.start |
d93a69672362
more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents:
43506
diff
changeset
|
250 |
val j = r.stop - range.start |
44056
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
251 |
val s1 = str.substring(0, i) |
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
252 |
val s2 = str.substring(i, j) |
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
253 |
val s3 = str.substring(j) |
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
254 |
|
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
255 |
if (!s1.isEmpty) gfx.drawString(s1, x1, y) |
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
256 |
|
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
257 |
val astr = new AttributedString(s2) |
43759
d93a69672362
more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents:
43506
diff
changeset
|
258 |
astr.addAttribute(TextAttribute.FONT, chunk_font) |
44056
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
259 |
astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor) |
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
260 |
astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON) |
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
261 |
gfx.drawString(astr.getIterator, x1 + string_width(s1), y) |
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
262 |
|
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
263 |
if (!s3.isEmpty) |
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
264 |
gfx.drawString(s3, x1 + string_width(str.substring(0, j)), y) |
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
265 |
|
43759
d93a69672362
more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents:
43506
diff
changeset
|
266 |
case _ => |
d93a69672362
more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents:
43506
diff
changeset
|
267 |
gfx.drawString(str, x1, y) |
43382 | 268 |
} |
44056
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
269 |
x1 += string_width(str) |
43382 | 270 |
} |
271 |
} |
|
272 |
w += chunk.width |
|
273 |
chunk = chunk.next.asInstanceOf[Chunk] |
|
274 |
} |
|
275 |
w |
|
276 |
} |
|
277 |
||
43381 | 278 |
private val text_painter = new TextAreaExtension |
279 |
{ |
|
280 |
override def paintScreenLineRange(gfx: Graphics2D, |
|
281 |
first_line: Int, last_line: Int, physical_lines: Array[Int], |
|
43382 | 282 |
start: Array[Int], end: Array[Int], y: Int, line_height: Int) |
43381 | 283 |
{ |
46220
663251a395c2
more explicit/robust treatment of common snapshot;
wenzelm
parents:
46205
diff
changeset
|
284 |
robust_snapshot { snapshot => |
43381 | 285 |
val clip = gfx.getClip |
286 |
val x0 = text_area.getHorizontalOffset |
|
43382 | 287 |
val fm = text_area.getPainter.getFontMetrics |
288 |
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
|
289 |
|
43382 | 290 |
val infos = line_infos(physical_lines.iterator.filter(i => i != -1)) |
43381 | 291 |
for (i <- 0 until physical_lines.length) { |
292 |
if (physical_lines(i) != -1) { |
|
43392 | 293 |
val x1 = |
294 |
infos.get(start(i)) match { |
|
295 |
case None => x0 |
|
296 |
case Some(chunk) => |
|
297 |
gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height) |
|
46220
663251a395c2
more explicit/robust treatment of common snapshot;
wenzelm
parents:
46205
diff
changeset
|
298 |
val w = paint_chunk_list(snapshot, gfx, start(i), chunk, x0, y0).toInt |
43392 | 299 |
x0 + w.toInt |
300 |
} |
|
301 |
gfx.clipRect(x1, 0, Integer.MAX_VALUE, Integer.MAX_VALUE) |
|
302 |
orig_text_painter.paintValidLine(gfx, |
|
303 |
first_line + i, physical_lines(i), start(i), end(i), y + line_height * i) |
|
304 |
gfx.setClip(clip) |
|
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
305 |
} |
43381 | 306 |
y0 += line_height |
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
307 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
308 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
309 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
310 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
311 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
312 |
|
43435
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
313 |
/* foreground */ |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
314 |
|
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
315 |
private val foreground_painter = new TextAreaExtension |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
316 |
{ |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
317 |
override def paintScreenLineRange(gfx: Graphics2D, |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
318 |
first_line: Int, last_line: Int, physical_lines: Array[Int], |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
319 |
start: Array[Int], end: Array[Int], y: Int, line_height: Int) |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
320 |
{ |
46220
663251a395c2
more explicit/robust treatment of common snapshot;
wenzelm
parents:
46205
diff
changeset
|
321 |
robust_snapshot { snapshot => |
43435
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
322 |
for (i <- 0 until physical_lines.length) { |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
323 |
if (physical_lines(i) != -1) { |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
324 |
val line_range = doc_view.proper_line_range(start(i), end(i)) |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
325 |
|
44545
3c40007aa031
transparent foreground color for quoted entities;
wenzelm
parents:
44056
diff
changeset
|
326 |
// foreground color |
3c40007aa031
transparent foreground color for quoted entities;
wenzelm
parents:
44056
diff
changeset
|
327 |
for { |
46178
1c5c88f6feb5
clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents:
46166
diff
changeset
|
328 |
Text.Info(range, color) <- Isabelle_Rendering.foreground(snapshot, line_range) |
46204 | 329 |
r <- gfx_range(range) |
44545
3c40007aa031
transparent foreground color for quoted entities;
wenzelm
parents:
44056
diff
changeset
|
330 |
} { |
3c40007aa031
transparent foreground color for quoted entities;
wenzelm
parents:
44056
diff
changeset
|
331 |
gfx.setColor(color) |
3c40007aa031
transparent foreground color for quoted entities;
wenzelm
parents:
44056
diff
changeset
|
332 |
gfx.fillRect(r.x, y + i * line_height, r.length, line_height) |
3c40007aa031
transparent foreground color for quoted entities;
wenzelm
parents:
44056
diff
changeset
|
333 |
} |
3c40007aa031
transparent foreground color for quoted entities;
wenzelm
parents:
44056
diff
changeset
|
334 |
|
43435
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
335 |
// highlighted range -- potentially from other snapshot |
46205 | 336 |
for { |
337 |
info <- doc_view.highlight_range() |
|
338 |
Text.Info(range, color) <- info.try_restrict(line_range) |
|
339 |
r <- gfx_range(range) |
|
340 |
} { |
|
341 |
gfx.setColor(color) |
|
342 |
gfx.fillRect(r.x, y + i * line_height, r.length, line_height) |
|
43435
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
343 |
} |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
344 |
} |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
345 |
} |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
346 |
} |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
347 |
} |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
348 |
} |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
349 |
|
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
350 |
|
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
351 |
/* caret -- outside of text range */ |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
352 |
|
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
353 |
private class Caret_Painter(before: Boolean) extends TextAreaExtension |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
354 |
{ |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
355 |
override def paintValidLine(gfx: Graphics2D, |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
356 |
screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int) |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
357 |
{ |
46220
663251a395c2
more explicit/robust treatment of common snapshot;
wenzelm
parents:
46205
diff
changeset
|
358 |
robust_snapshot { _ => |
43404 | 359 |
if (before) gfx.clipRect(0, 0, 0, 0) |
360 |
else gfx.setClip(painter_clip) |
|
361 |
} |
|
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
362 |
} |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
363 |
} |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
364 |
|
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
365 |
private val before_caret_painter1 = new Caret_Painter(true) |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
366 |
private val after_caret_painter1 = new Caret_Painter(false) |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
367 |
private val before_caret_painter2 = new Caret_Painter(true) |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
368 |
private val after_caret_painter2 = new Caret_Painter(false) |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
369 |
|
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
370 |
private val caret_painter = new TextAreaExtension |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
371 |
{ |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
372 |
override def paintValidLine(gfx: Graphics2D, |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
373 |
screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int) |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
374 |
{ |
46220
663251a395c2
more explicit/robust treatment of common snapshot;
wenzelm
parents:
46205
diff
changeset
|
375 |
robust_snapshot { _ => |
43398
c3e2a361b418
more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
wenzelm
parents:
43396
diff
changeset
|
376 |
if (text_area.hasFocus) { |
c3e2a361b418
more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
wenzelm
parents:
43396
diff
changeset
|
377 |
val caret = text_area.getCaretPosition |
c3e2a361b418
more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
wenzelm
parents:
43396
diff
changeset
|
378 |
if (start <= caret && caret == end - 1) { |
c3e2a361b418
more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
wenzelm
parents:
43396
diff
changeset
|
379 |
val painter = text_area.getPainter |
c3e2a361b418
more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
wenzelm
parents:
43396
diff
changeset
|
380 |
val fm = painter.getFontMetrics |
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
381 |
|
43398
c3e2a361b418
more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
wenzelm
parents:
43396
diff
changeset
|
382 |
val offset = caret - text_area.getLineStartOffset(physical_line) |
c3e2a361b418
more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
wenzelm
parents:
43396
diff
changeset
|
383 |
val x = text_area.offsetToXY(physical_line, offset).x |
c3e2a361b418
more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
wenzelm
parents:
43396
diff
changeset
|
384 |
gfx.setColor(painter.getCaretColor) |
c3e2a361b418
more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
wenzelm
parents:
43396
diff
changeset
|
385 |
gfx.drawRect(x, y, char_width() - 1, fm.getHeight - 1) |
c3e2a361b418
more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
wenzelm
parents:
43396
diff
changeset
|
386 |
} |
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
387 |
} |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
388 |
} |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
389 |
} |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
390 |
} |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
391 |
|
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
392 |
|
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
393 |
/* activation */ |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
394 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
395 |
def activate() |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
396 |
{ |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
397 |
val painter = text_area.getPainter |
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
398 |
painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state) |
43381 | 399 |
painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter) |
400 |
painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter) |
|
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
401 |
painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1) |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
402 |
painter.addExtension(TextAreaPainter.CARET_LAYER + 1, after_caret_painter1) |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
403 |
painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2) |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
404 |
painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2) |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
405 |
painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter) |
43435
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
406 |
painter.addExtension(500, foreground_painter) |
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
407 |
painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state) |
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
408 |
painter.removeExtension(orig_text_painter) |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
409 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
410 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
411 |
def deactivate() |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
412 |
{ |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
413 |
val painter = text_area.getPainter |
43396 | 414 |
painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter) |
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
415 |
painter.removeExtension(reset_state) |
43435
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
416 |
painter.removeExtension(foreground_painter) |
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
417 |
painter.removeExtension(caret_painter) |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
418 |
painter.removeExtension(after_caret_painter2) |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
419 |
painter.removeExtension(before_caret_painter2) |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
420 |
painter.removeExtension(after_caret_painter1) |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
421 |
painter.removeExtension(before_caret_painter1) |
43381 | 422 |
painter.removeExtension(text_painter) |
423 |
painter.removeExtension(background_painter) |
|
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
424 |
painter.removeExtension(set_state) |
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
425 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
426 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
427 |