author | wenzelm |
Fri, 21 Sep 2012 16:50:44 +0200 | |
changeset 49493 | db58490a68ac |
parent 49492 | 2e3e7ea5ce8e |
child 49700 | 2d1cbdf6a68b |
permissions | -rw-r--r-- |
49411 | 1 |
/* Title: Tools/jEdit/src/rich_text_area.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 |
|
49411 | 4 |
Enhanced version of jEdit text area, with rich text rendering, |
5 |
tooltips, hyperlinks etc. |
|
43369
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 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
8 |
package isabelle.jedit |
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 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
11 |
import isabelle._ |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
12 |
|
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
13 |
import java.awt.{Graphics2D, Shape, Window, Color} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
14 |
import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent, |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
15 |
FocusAdapter, FocusEvent, WindowEvent, WindowAdapter} |
43392 | 16 |
import java.awt.font.TextAttribute |
17 |
import java.text.AttributedString |
|
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
18 |
import java.util.ArrayList |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
19 |
|
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
20 |
import org.gjt.sp.util.Log |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
21 |
import org.gjt.sp.jedit.{OperatingSystem, Debug, View} |
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
22 |
import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk} |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
23 |
import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, TextArea} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
24 |
|
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
25 |
|
49492 | 26 |
class Rich_Text_Area( |
27 |
view: View, |
|
28 |
text_area: TextArea, |
|
29 |
get_rendering: () => Isabelle_Rendering, |
|
30 |
hovering: Boolean) |
|
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
31 |
{ |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
32 |
private val buffer = text_area.getBuffer |
43369
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 |
|
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
35 |
/* robust extension body */ |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
36 |
|
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
37 |
def robust_body[A](default: A)(body: => A): A = |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
38 |
{ |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
39 |
try { |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
40 |
Swing_Thread.require() |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
41 |
if (buffer == text_area.getBuffer) body |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
42 |
else { |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
43 |
Log.log(Log.ERROR, this, ERROR("Implicit change of text area buffer")) |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
44 |
default |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
45 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
46 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
47 |
catch { case t: Throwable => Log.log(Log.ERROR, this, t); default } |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
48 |
} |
43376
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
49 |
|
43392 | 50 |
|
51 |
/* original painters */ |
|
52 |
||
53 |
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
|
54 |
{ |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
55 |
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
|
56 |
match { |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
57 |
case List(x) => x |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
58 |
case _ => error("Expected exactly one " + name) |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
59 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
60 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
61 |
|
43392 | 62 |
private val orig_text_painter = |
63 |
pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText") |
|
64 |
||
65 |
||
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
66 |
/* common painter state */ |
43381 | 67 |
|
49356 | 68 |
@volatile private var painter_rendering: Isabelle_Rendering = null |
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
69 |
@volatile private var painter_clip: Shape = null |
43381 | 70 |
|
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
71 |
private val set_state = new TextAreaExtension |
43381 | 72 |
{ |
73 |
override def paintScreenLineRange(gfx: Graphics2D, |
|
74 |
first_line: Int, last_line: Int, physical_lines: Array[Int], |
|
75 |
start: Array[Int], end: Array[Int], y: Int, line_height: Int) |
|
76 |
{ |
|
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
77 |
painter_rendering = get_rendering() |
46220
663251a395c2
more explicit/robust treatment of common snapshot;
wenzelm
parents:
46205
diff
changeset
|
78 |
painter_clip = gfx.getClip |
43381 | 79 |
} |
80 |
} |
|
81 |
||
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
82 |
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
|
83 |
{ |
43381 | 84 |
override def paintScreenLineRange(gfx: Graphics2D, |
85 |
first_line: Int, last_line: Int, physical_lines: Array[Int], |
|
86 |
start: Array[Int], end: Array[Int], y: Int, line_height: Int) |
|
87 |
{ |
|
49356 | 88 |
painter_rendering = null |
46220
663251a395c2
more explicit/robust treatment of common snapshot;
wenzelm
parents:
46205
diff
changeset
|
89 |
painter_clip = null |
43381 | 90 |
} |
91 |
} |
|
92 |
||
49473 | 93 |
def robust_rendering(body: Isabelle_Rendering => Unit) |
46220
663251a395c2
more explicit/robust treatment of common snapshot;
wenzelm
parents:
46205
diff
changeset
|
94 |
{ |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
95 |
robust_body(()) { body(painter_rendering) } |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
96 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
97 |
|
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
98 |
|
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
99 |
/* active areas within the text */ |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
100 |
|
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
101 |
private class Active_Area[A]( |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
102 |
rendering: Isabelle_Rendering => Text.Range => Option[Text.Info[A]]) |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
103 |
{ |
49493
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
104 |
private var the_text_info: Option[(String, Text.Info[A])] = None |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
105 |
|
49493
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
106 |
def text_info: Option[(String, Text.Info[A])] = the_text_info |
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
107 |
def info: Option[Text.Info[A]] = the_text_info.map(_._2) |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
108 |
|
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
109 |
def update(new_info: Option[Text.Info[A]]) |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
110 |
{ |
49493
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
111 |
val old_text_info = the_text_info |
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
112 |
val new_text_info = |
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
113 |
new_info.map(info => (text_area.getText(info.range.start, info.range.length), info)) |
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
114 |
|
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
115 |
if (new_text_info != old_text_info) { |
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
116 |
for { |
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
117 |
r0 <- JEdit_Lib.visible_range(text_area) |
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
118 |
opt <- List(old_text_info, new_text_info) |
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
119 |
(_, Text.Info(r1, _)) <- opt |
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
120 |
r2 <- r1.try_restrict(r0) // FIXME more precise?! |
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
121 |
} JEdit_Lib.invalidate_range(text_area, r2) |
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
122 |
the_text_info = new_text_info |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
123 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
124 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
125 |
|
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
126 |
def update_rendering(r: Isabelle_Rendering, range: Text.Range) |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
127 |
{ update(rendering(r)(range)) } |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
128 |
|
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
129 |
def reset { update(None) } |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
130 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
131 |
|
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
132 |
// owned by Swing thread |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
133 |
|
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
134 |
private var control: Boolean = false |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
135 |
|
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
136 |
private val highlight_area = new Active_Area[Color]((r: Isabelle_Rendering) => r.highlight _) |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
137 |
private val hyperlink_area = new Active_Area[Hyperlink]((r: Isabelle_Rendering) => r.hyperlink _) |
49493
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
138 |
private val sendback_area = |
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
139 |
new Active_Area[Document.Exec_ID]((r: Isabelle_Rendering) => r.sendback _) |
49492 | 140 |
|
141 |
private val active_areas = |
|
142 |
List((highlight_area, true), (hyperlink_area, true), (sendback_area, false)) |
|
143 |
private def active_reset(): Unit = active_areas.foreach(_._1.reset) |
|
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
144 |
|
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
145 |
private val focus_listener = new FocusAdapter { |
49424 | 146 |
override def focusLost(e: FocusEvent) { robust_body(()) { active_reset() } } |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
147 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
148 |
|
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
149 |
private val window_listener = new WindowAdapter { |
49424 | 150 |
override def windowIconified(e: WindowEvent) { robust_body(()) { active_reset() } } |
151 |
override def windowDeactivated(e: WindowEvent) { robust_body(()) { active_reset() } } |
|
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
152 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
153 |
|
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
154 |
private val mouse_listener = new MouseAdapter { |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
155 |
override def mouseClicked(e: MouseEvent) { |
49424 | 156 |
robust_body(()) { |
157 |
hyperlink_area.info match { |
|
49492 | 158 |
case Some(Text.Info(_, link)) => link.follow(view) |
159 |
case None => |
|
160 |
} |
|
49493
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
161 |
sendback_area.text_info match { |
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
162 |
case Some((text, Text.Info(_, id))) => Sendback.activate(view, text, id) |
49424 | 163 |
case None => |
164 |
} |
|
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
165 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
166 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
167 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
168 |
|
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
169 |
private val mouse_motion_listener = new MouseMotionAdapter { |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
170 |
override def mouseMoved(e: MouseEvent) { |
49424 | 171 |
robust_body(()) { |
172 |
control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown |
|
49492 | 173 |
|
174 |
if ((control || hovering) && !buffer.isLoading) { |
|
49424 | 175 |
JEdit_Lib.buffer_lock(buffer) { |
176 |
val rendering = get_rendering() |
|
177 |
val mouse_offset = text_area.xyToOffset(e.getX(), e.getY()) |
|
178 |
val mouse_range = JEdit_Lib.point_range(buffer, mouse_offset) |
|
49492 | 179 |
for ((area, require_control) <- active_areas) |
180 |
{ |
|
181 |
if (control == require_control) |
|
182 |
area.update_rendering(rendering, mouse_range) |
|
183 |
else area.reset |
|
184 |
} |
|
49424 | 185 |
} |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
186 |
} |
49424 | 187 |
else active_reset() |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
188 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
189 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
190 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
191 |
|
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
192 |
|
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
193 |
/* tooltips */ |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
194 |
|
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
195 |
private val tooltip_painter = new TextAreaExtension |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
196 |
{ |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
197 |
override def getToolTipText(x: Int, y: Int): String = |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
198 |
{ |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
199 |
robust_body(null: String) { |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
200 |
val rendering = get_rendering() |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
201 |
val offset = text_area.xyToOffset(x, y) |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
202 |
val range = Text.Range(offset, offset + 1) |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
203 |
val tip = |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
204 |
if (control) rendering.tooltip(range) |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
205 |
else rendering.tooltip_message(range) |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
206 |
tip.map(Isabelle.tooltip(_)) getOrElse null |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
207 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
208 |
} |
46220
663251a395c2
more explicit/robust treatment of common snapshot;
wenzelm
parents:
46205
diff
changeset
|
209 |
} |
663251a395c2
more explicit/robust treatment of common snapshot;
wenzelm
parents:
46205
diff
changeset
|
210 |
|
43381 | 211 |
|
212 |
/* text background */ |
|
43376
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
213 |
|
43381 | 214 |
private val background_painter = new TextAreaExtension |
215 |
{ |
|
216 |
override def paintScreenLineRange(gfx: Graphics2D, |
|
217 |
first_line: Int, last_line: Int, physical_lines: Array[Int], |
|
218 |
start: Array[Int], end: Array[Int], y: Int, line_height: Int) |
|
219 |
{ |
|
49356 | 220 |
robust_rendering { rendering => |
43381 | 221 |
val ascent = text_area.getPainter.getFontMetrics.getAscent |
43376
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
222 |
|
43381 | 223 |
for (i <- 0 until physical_lines.length) { |
224 |
if (physical_lines(i) != -1) { |
|
49408 | 225 |
val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i)) |
43376
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
226 |
|
49473 | 227 |
// line background color |
228 |
for { (color, separator) <- rendering.line_background(line_range) } |
|
229 |
{ |
|
230 |
gfx.setColor(color) |
|
49475 | 231 |
val sep = if (separator) (2 min (line_height / 2)) else 0 |
232 |
gfx.fillRect(0, y + i * line_height, text_area.getWidth, line_height - sep) |
|
49473 | 233 |
} |
234 |
||
46166 | 235 |
// background color (1) |
43381 | 236 |
for { |
49356 | 237 |
Text.Info(range, color) <- rendering.background1(line_range) |
49409 | 238 |
r <- JEdit_Lib.gfx_range(text_area, range) |
43381 | 239 |
} { |
240 |
gfx.setColor(color) |
|
241 |
gfx.fillRect(r.x, y + i * line_height, r.length, line_height) |
|
242 |
} |
|
43376
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
243 |
|
49492 | 244 |
// sendback range -- potentially from other snapshot |
245 |
for { |
|
246 |
info <- sendback_area.info |
|
247 |
Text.Info(range, _) <- info.try_restrict(line_range) |
|
248 |
r <- JEdit_Lib.gfx_range(text_area, range) |
|
249 |
} { |
|
250 |
gfx.setColor(rendering.sendback_active_color) |
|
251 |
gfx.fillRect(r.x, y + i * line_height, r.length, line_height) |
|
252 |
} |
|
253 |
||
46166 | 254 |
// background color (2) |
43381 | 255 |
for { |
49356 | 256 |
Text.Info(range, color) <- rendering.background2(line_range) |
49409 | 257 |
r <- JEdit_Lib.gfx_range(text_area, range) |
43381 | 258 |
} { |
259 |
gfx.setColor(color) |
|
260 |
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
|
261 |
} |
43381 | 262 |
|
263 |
// squiggly underline |
|
264 |
for { |
|
49356 | 265 |
Text.Info(range, color) <- rendering.squiggly_underline(line_range) |
49409 | 266 |
r <- JEdit_Lib.gfx_range(text_area, range) |
43381 | 267 |
} { |
268 |
gfx.setColor(color) |
|
269 |
val x0 = (r.x / 2) * 2 |
|
270 |
val y0 = r.y + ascent + 1 |
|
271 |
for (x1 <- Range(x0, x0 + r.length, 2)) { |
|
272 |
val y1 = if (x1 % 4 < 2) y0 else y0 + 1 |
|
273 |
gfx.drawLine(x1, y1, x1 + 1, y1) |
|
43376
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
274 |
} |
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
275 |
} |
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
276 |
} |
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
277 |
} |
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
278 |
} |
43381 | 279 |
} |
280 |
} |
|
281 |
||
282 |
||
283 |
/* text */ |
|
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
284 |
|
49356 | 285 |
private def paint_chunk_list(rendering: Isabelle_Rendering, |
43505 | 286 |
gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float = |
43382 | 287 |
{ |
288 |
val clip_rect = gfx.getClipBounds |
|
43392 | 289 |
val painter = text_area.getPainter |
290 |
val font_context = painter.getFontRenderContext |
|
43382 | 291 |
|
292 |
var w = 0.0f |
|
293 |
var chunk = head |
|
294 |
while (chunk != null) { |
|
43505 | 295 |
val chunk_offset = line_start + chunk.offset |
43382 | 296 |
if (x + w + chunk.width > clip_rect.x && |
43506 | 297 |
x + w < clip_rect.x + clip_rect.width && chunk.accessable) |
43382 | 298 |
{ |
43505 | 299 |
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
|
300 |
val chunk_str = if (chunk.str == null) " " * chunk.length else chunk.str |
43382 | 301 |
val chunk_font = chunk.style.getFont |
302 |
val chunk_color = chunk.style.getForegroundColor |
|
303 |
||
44056
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
304 |
def string_width(s: String): Float = |
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
305 |
if (s.isEmpty) 0.0f |
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
306 |
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
|
307 |
|
43448
90aec5043461
more robust caret painting wrt. surrogate characters;
wenzelm
parents:
43435
diff
changeset
|
308 |
val caret_range = |
49407 | 309 |
if (text_area.isCaretVisible) |
310 |
JEdit_Lib.point_range(buffer, text_area.getCaretPosition) |
|
43448
90aec5043461
more robust caret painting wrt. surrogate characters;
wenzelm
parents:
43435
diff
changeset
|
311 |
else Text.Range(-1) |
90aec5043461
more robust caret painting wrt. surrogate characters;
wenzelm
parents:
43435
diff
changeset
|
312 |
|
43426
24e2e2f0032b
more explicit treatment of ranges after revert/convert, which may well distort the overall start/end positions;
wenzelm
parents:
43419
diff
changeset
|
313 |
val markup = |
43428
b41dea5772c6
more robust treatment of partial range restriction;
wenzelm
parents:
43426
diff
changeset
|
314 |
for { |
49356 | 315 |
r1 <- rendering.text_color(chunk_range, chunk_color) |
43450 | 316 |
r2 <- r1.try_restrict(chunk_range) |
317 |
} yield r2 |
|
43382 | 318 |
|
43759
d93a69672362
more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents:
43506
diff
changeset
|
319 |
val padded_markup = |
d93a69672362
more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents:
43506
diff
changeset
|
320 |
if (markup.isEmpty) |
46197
e4da482283ef
tuned text_color: cumulate with explicit default color;
wenzelm
parents:
46178
diff
changeset
|
321 |
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
|
322 |
else |
46197
e4da482283ef
tuned text_color: cumulate with explicit default color;
wenzelm
parents:
46178
diff
changeset
|
323 |
Iterator( |
e4da482283ef
tuned text_color: cumulate with explicit default color;
wenzelm
parents:
46178
diff
changeset
|
324 |
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
|
325 |
markup.iterator ++ |
46197
e4da482283ef
tuned text_color: cumulate with explicit default color;
wenzelm
parents:
46178
diff
changeset
|
326 |
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
|
327 |
|
43450 | 328 |
var x1 = x + w |
43382 | 329 |
gfx.setFont(chunk_font) |
46197
e4da482283ef
tuned text_color: cumulate with explicit default color;
wenzelm
parents:
46178
diff
changeset
|
330 |
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
|
331 |
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
|
332 |
gfx.setColor(color) |
43448
90aec5043461
more robust caret painting wrt. surrogate characters;
wenzelm
parents:
43435
diff
changeset
|
333 |
|
43759
d93a69672362
more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents:
43506
diff
changeset
|
334 |
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
|
335 |
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
|
336 |
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
|
337 |
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
|
338 |
val s1 = str.substring(0, i) |
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
339 |
val s2 = str.substring(i, j) |
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
340 |
val s3 = str.substring(j) |
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
341 |
|
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
342 |
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
|
343 |
|
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
344 |
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
|
345 |
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
|
346 |
astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor) |
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
347 |
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
|
348 |
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
|
349 |
|
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
350 |
if (!s3.isEmpty) |
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
351 |
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
|
352 |
|
43759
d93a69672362
more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents:
43506
diff
changeset
|
353 |
case _ => |
d93a69672362
more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents:
43506
diff
changeset
|
354 |
gfx.drawString(str, x1, y) |
43382 | 355 |
} |
44056
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
356 |
x1 += string_width(str) |
43382 | 357 |
} |
358 |
} |
|
359 |
w += chunk.width |
|
360 |
chunk = chunk.next.asInstanceOf[Chunk] |
|
361 |
} |
|
362 |
w |
|
363 |
} |
|
364 |
||
43381 | 365 |
private val text_painter = new TextAreaExtension |
366 |
{ |
|
367 |
override def paintScreenLineRange(gfx: Graphics2D, |
|
368 |
first_line: Int, last_line: Int, physical_lines: Array[Int], |
|
43382 | 369 |
start: Array[Int], end: Array[Int], y: Int, line_height: Int) |
43381 | 370 |
{ |
49356 | 371 |
robust_rendering { rendering => |
43381 | 372 |
val clip = gfx.getClip |
373 |
val x0 = text_area.getHorizontalOffset |
|
43382 | 374 |
val fm = text_area.getPainter.getFontMetrics |
375 |
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
|
376 |
|
43381 | 377 |
for (i <- 0 until physical_lines.length) { |
49097
4e5e48c589ea
more direct access to all-important chunks for text painting;
wenzelm
parents:
48921
diff
changeset
|
378 |
val line = physical_lines(i) |
4e5e48c589ea
more direct access to all-important chunks for text painting;
wenzelm
parents:
48921
diff
changeset
|
379 |
if (line != -1) { |
4e5e48c589ea
more direct access to all-important chunks for text painting;
wenzelm
parents:
48921
diff
changeset
|
380 |
val screen_line = first_line + i |
4e5e48c589ea
more direct access to all-important chunks for text painting;
wenzelm
parents:
48921
diff
changeset
|
381 |
val chunks = text_area.getChunksOfScreenLine(screen_line) |
4e5e48c589ea
more direct access to all-important chunks for text painting;
wenzelm
parents:
48921
diff
changeset
|
382 |
if (chunks != null) { |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
383 |
val line_start = buffer.getLineStartOffset(line) |
49097
4e5e48c589ea
more direct access to all-important chunks for text painting;
wenzelm
parents:
48921
diff
changeset
|
384 |
gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height) |
49356 | 385 |
val w = paint_chunk_list(rendering, gfx, line_start, chunks, x0, y0).toInt |
49097
4e5e48c589ea
more direct access to all-important chunks for text painting;
wenzelm
parents:
48921
diff
changeset
|
386 |
gfx.clipRect(x0 + w.toInt, 0, Integer.MAX_VALUE, Integer.MAX_VALUE) |
4e5e48c589ea
more direct access to all-important chunks for text painting;
wenzelm
parents:
48921
diff
changeset
|
387 |
orig_text_painter.paintValidLine(gfx, |
4e5e48c589ea
more direct access to all-important chunks for text painting;
wenzelm
parents:
48921
diff
changeset
|
388 |
screen_line, line, start(i), end(i), y + line_height * i) |
4e5e48c589ea
more direct access to all-important chunks for text painting;
wenzelm
parents:
48921
diff
changeset
|
389 |
gfx.setClip(clip) |
4e5e48c589ea
more direct access to all-important chunks for text painting;
wenzelm
parents:
48921
diff
changeset
|
390 |
} |
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
391 |
} |
43381 | 392 |
y0 += line_height |
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
393 |
} |
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 |
} |
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 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
398 |
|
43435
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
399 |
/* foreground */ |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
400 |
|
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
401 |
private val foreground_painter = new TextAreaExtension |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
402 |
{ |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
403 |
override def paintScreenLineRange(gfx: Graphics2D, |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
404 |
first_line: Int, last_line: Int, physical_lines: Array[Int], |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
405 |
start: Array[Int], end: Array[Int], y: Int, line_height: Int) |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
406 |
{ |
49356 | 407 |
robust_rendering { rendering => |
43435
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
408 |
for (i <- 0 until physical_lines.length) { |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
409 |
if (physical_lines(i) != -1) { |
49408 | 410 |
val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i)) |
43435
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
411 |
|
44545
3c40007aa031
transparent foreground color for quoted entities;
wenzelm
parents:
44056
diff
changeset
|
412 |
// foreground color |
3c40007aa031
transparent foreground color for quoted entities;
wenzelm
parents:
44056
diff
changeset
|
413 |
for { |
49356 | 414 |
Text.Info(range, color) <- rendering.foreground(line_range) |
49409 | 415 |
r <- JEdit_Lib.gfx_range(text_area, range) |
44545
3c40007aa031
transparent foreground color for quoted entities;
wenzelm
parents:
44056
diff
changeset
|
416 |
} { |
3c40007aa031
transparent foreground color for quoted entities;
wenzelm
parents:
44056
diff
changeset
|
417 |
gfx.setColor(color) |
3c40007aa031
transparent foreground color for quoted entities;
wenzelm
parents:
44056
diff
changeset
|
418 |
gfx.fillRect(r.x, y + i * line_height, r.length, line_height) |
3c40007aa031
transparent foreground color for quoted entities;
wenzelm
parents:
44056
diff
changeset
|
419 |
} |
3c40007aa031
transparent foreground color for quoted entities;
wenzelm
parents:
44056
diff
changeset
|
420 |
|
49357 | 421 |
// highlight range -- potentially from other snapshot |
46205 | 422 |
for { |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
423 |
info <- highlight_area.info |
46205 | 424 |
Text.Info(range, color) <- info.try_restrict(line_range) |
49409 | 425 |
r <- JEdit_Lib.gfx_range(text_area, range) |
46205 | 426 |
} { |
427 |
gfx.setColor(color) |
|
428 |
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
|
429 |
} |
48921
5d8d409b897e
support for direct hyperlinks, without the Hyperlinks plugin;
wenzelm
parents:
47471
diff
changeset
|
430 |
|
5d8d409b897e
support for direct hyperlinks, without the Hyperlinks plugin;
wenzelm
parents:
47471
diff
changeset
|
431 |
// hyperlink range -- potentially from other snapshot |
5d8d409b897e
support for direct hyperlinks, without the Hyperlinks plugin;
wenzelm
parents:
47471
diff
changeset
|
432 |
for { |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
433 |
info <- hyperlink_area.info |
48921
5d8d409b897e
support for direct hyperlinks, without the Hyperlinks plugin;
wenzelm
parents:
47471
diff
changeset
|
434 |
Text.Info(range, _) <- info.try_restrict(line_range) |
49409 | 435 |
r <- JEdit_Lib.gfx_range(text_area, range) |
48921
5d8d409b897e
support for direct hyperlinks, without the Hyperlinks plugin;
wenzelm
parents:
47471
diff
changeset
|
436 |
} { |
49356 | 437 |
gfx.setColor(rendering.hyperlink_color) |
48921
5d8d409b897e
support for direct hyperlinks, without the Hyperlinks plugin;
wenzelm
parents:
47471
diff
changeset
|
438 |
gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1) |
5d8d409b897e
support for direct hyperlinks, without the Hyperlinks plugin;
wenzelm
parents:
47471
diff
changeset
|
439 |
} |
43435
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
440 |
} |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
441 |
} |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
442 |
} |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
443 |
} |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
444 |
} |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
445 |
|
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
446 |
|
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
447 |
/* 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
|
448 |
|
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
449 |
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
|
450 |
{ |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
451 |
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
|
452 |
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
|
453 |
{ |
49356 | 454 |
robust_rendering { _ => |
43404 | 455 |
if (before) gfx.clipRect(0, 0, 0, 0) |
456 |
else gfx.setClip(painter_clip) |
|
457 |
} |
|
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
458 |
} |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
459 |
} |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
460 |
|
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
461 |
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
|
462 |
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
|
463 |
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
|
464 |
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
|
465 |
|
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
466 |
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
|
467 |
{ |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
468 |
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
|
469 |
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
|
470 |
{ |
49356 | 471 |
robust_rendering { _ => |
47471
d6a1b5aeb4b1
use official TextArea.isCaretVisible and thus follow the "blink" flag;
wenzelm
parents:
47027
diff
changeset
|
472 |
if (text_area.isCaretVisible) { |
43398
c3e2a361b418
more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
wenzelm
parents:
43396
diff
changeset
|
473 |
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
|
474 |
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
|
475 |
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
|
476 |
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
|
477 |
|
43398
c3e2a361b418
more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
wenzelm
parents:
43396
diff
changeset
|
478 |
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
|
479 |
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
|
480 |
gfx.setColor(painter.getCaretColor) |
49409 | 481 |
gfx.drawRect(x, y, JEdit_Lib.char_width(text_area) - 1, fm.getHeight - 1) |
43398
c3e2a361b418
more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
wenzelm
parents:
43396
diff
changeset
|
482 |
} |
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
483 |
} |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
484 |
} |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
485 |
} |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
486 |
} |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
487 |
|
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
488 |
|
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
489 |
/* activation */ |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
490 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
491 |
def activate() |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
492 |
{ |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
493 |
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
|
494 |
painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state) |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
495 |
painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, tooltip_painter) |
43381 | 496 |
painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter) |
497 |
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
|
498 |
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
|
499 |
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
|
500 |
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
|
501 |
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
|
502 |
painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter) |
43435
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
503 |
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
|
504 |
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
|
505 |
painter.removeExtension(orig_text_painter) |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
506 |
painter.addMouseListener(mouse_listener) |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
507 |
painter.addMouseMotionListener(mouse_motion_listener) |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
508 |
text_area.addFocusListener(focus_listener) |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
509 |
view.addWindowListener(window_listener) |
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
510 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
511 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
512 |
def deactivate() |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
513 |
{ |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
514 |
val painter = text_area.getPainter |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
515 |
view.removeWindowListener(window_listener) |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
516 |
text_area.removeFocusListener(focus_listener) |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
517 |
painter.removeMouseMotionListener(mouse_motion_listener) |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
518 |
painter.removeMouseListener(mouse_listener) |
43396 | 519 |
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
|
520 |
painter.removeExtension(reset_state) |
43435
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
521 |
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
|
522 |
painter.removeExtension(caret_painter) |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
523 |
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
|
524 |
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
|
525 |
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
|
526 |
painter.removeExtension(before_caret_painter1) |
43381 | 527 |
painter.removeExtension(text_painter) |
528 |
painter.removeExtension(background_painter) |
|
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
529 |
painter.removeExtension(tooltip_painter) |
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
530 |
painter.removeExtension(set_state) |
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
531 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
532 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
533 |