author | wenzelm |
Fri, 25 Jun 2021 21:16:53 +0200 | |
changeset 73877 | d9ebbfe099a8 |
parent 73876 | e6c9c1c3f580 |
child 73880 | 9ce206f6e8c6 |
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 |
|
72927
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
13 |
import java.awt.{Graphics2D, Shape, Color, Point, Cursor, MouseInfo} |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
14 |
import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent, |
72927
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
15 |
FocusAdapter, FocusEvent, WindowEvent, WindowAdapter, KeyEvent} |
43392 | 16 |
import java.awt.font.TextAttribute |
56322
f9ad26836516
check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;
wenzelm
parents:
56321
diff
changeset
|
17 |
import javax.swing.SwingUtilities |
43392 | 18 |
import java.text.AttributedString |
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
19 |
|
56883
38c6b70e5e53
common support for search field, which is actually a light-weight Highlighter;
wenzelm
parents:
56662
diff
changeset
|
20 |
import scala.util.matching.Regex |
38c6b70e5e53
common support for search field, which is actually a light-weight Highlighter;
wenzelm
parents:
56662
diff
changeset
|
21 |
|
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
22 |
import org.gjt.sp.util.Log |
72898 | 23 |
import org.gjt.sp.jedit.View |
24 |
import org.gjt.sp.jedit.syntax.Chunk |
|
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
25 |
import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, TextArea} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
26 |
|
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
27 |
|
49492 | 28 |
class Rich_Text_Area( |
29 |
view: View, |
|
30 |
text_area: TextArea, |
|
64621 | 31 |
get_rendering: () => JEdit_Rendering, |
50915
12de8ea66f54
close tooltip after Active.action, to make it look more interactive (notably due to lack of dynamic update);
wenzelm
parents:
50849
diff
changeset
|
32 |
close_action: () => Unit, |
56883
38c6b70e5e53
common support for search field, which is actually a light-weight Highlighter;
wenzelm
parents:
56662
diff
changeset
|
33 |
get_search_pattern: () => Option[Regex], |
63028 | 34 |
caret_update: () => Unit, |
50306 | 35 |
caret_visible: Boolean, |
53179 | 36 |
enable_hovering: Boolean) |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
37 |
{ |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
38 |
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
|
39 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
40 |
|
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
41 |
/* robust extension body */ |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
42 |
|
64884
b2e78c0ce537
more robust: delay switches thread context from timer to GUI and may get out of sync with revoke operation;
wenzelm
parents:
64621
diff
changeset
|
43 |
def check_robust_body: Boolean = |
b2e78c0ce537
more robust: delay switches thread context from timer to GUI and may get out of sync with revoke operation;
wenzelm
parents:
64621
diff
changeset
|
44 |
GUI_Thread.require { buffer == text_area.getBuffer } |
b2e78c0ce537
more robust: delay switches thread context from timer to GUI and may get out of sync with revoke operation;
wenzelm
parents:
64621
diff
changeset
|
45 |
|
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
46 |
def robust_body[A](default: A)(body: => A): A = |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
47 |
{ |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
48 |
try { |
64884
b2e78c0ce537
more robust: delay switches thread context from timer to GUI and may get out of sync with revoke operation;
wenzelm
parents:
64621
diff
changeset
|
49 |
if (check_robust_body) body |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
50 |
else { |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
51 |
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
|
52 |
default |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
53 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
54 |
} |
50641 | 55 |
catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); default } |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
56 |
} |
43376
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
57 |
|
43392 | 58 |
|
59 |
/* original painters */ |
|
60 |
||
61 |
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
|
62 |
{ |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
63 |
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
|
64 |
match { |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
65 |
case List(x) => x |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
66 |
case _ => error("Expected exactly one " + name) |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
67 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
68 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
69 |
|
43392 | 70 |
private val orig_text_painter = |
71 |
pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText") |
|
72 |
||
73 |
||
72927
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
74 |
/* caret focus modifier */ |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
75 |
|
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
76 |
@volatile private var caret_focus_modifier = false |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
77 |
|
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
78 |
def caret_focus_range: Text.Range = |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
79 |
if (caret_focus_modifier) Text.Range.full |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
80 |
else JEdit_Lib.visible_range(text_area) getOrElse Text.Range.offside |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
81 |
|
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
82 |
private val key_listener = |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
83 |
JEdit_Lib.key_listener( |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
84 |
key_pressed = (evt: KeyEvent) => |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
85 |
{ |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
86 |
val mod = PIDE.options.string("jedit_focus_modifier") |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
87 |
val old = caret_focus_modifier |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
88 |
caret_focus_modifier = (mod.nonEmpty && mod == JEdit_Lib.modifier_string(evt)) |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
89 |
if (caret_focus_modifier != old) caret_update() |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
90 |
}, |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
91 |
key_released = _ => |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
92 |
{ |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
93 |
if (caret_focus_modifier) { |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
94 |
caret_focus_modifier = false |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
95 |
caret_update() |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
96 |
} |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
97 |
}) |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
98 |
|
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
99 |
|
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
100 |
/* common painter state */ |
43381 | 101 |
|
64621 | 102 |
@volatile private var painter_rendering: JEdit_Rendering = null |
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
103 |
@volatile private var painter_clip: Shape = null |
72900 | 104 |
@volatile private var caret_focus = Rendering.Focus.empty |
43381 | 105 |
|
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
106 |
private val set_state = new TextAreaExtension |
43381 | 107 |
{ |
108 |
override def paintScreenLineRange(gfx: Graphics2D, |
|
109 |
first_line: Int, last_line: Int, physical_lines: Array[Int], |
|
73340 | 110 |
start: Array[Int], end: Array[Int], y: Int, line_height: Int): Unit = |
43381 | 111 |
{ |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
112 |
painter_rendering = get_rendering() |
46220
663251a395c2
more explicit/robust treatment of common snapshot;
wenzelm
parents:
46205
diff
changeset
|
113 |
painter_clip = gfx.getClip |
62988 | 114 |
caret_focus = |
72927
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
115 |
if (caret_enabled && !painter_rendering.snapshot.is_outdated) { |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
116 |
painter_rendering.caret_focus(JEdit_Lib.caret_range(text_area), caret_focus_range) |
62988 | 117 |
} |
72927
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
118 |
else Rendering.Focus.empty |
43381 | 119 |
} |
120 |
} |
|
121 |
||
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
122 |
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
|
123 |
{ |
43381 | 124 |
override def paintScreenLineRange(gfx: Graphics2D, |
125 |
first_line: Int, last_line: Int, physical_lines: Array[Int], |
|
73340 | 126 |
start: Array[Int], end: Array[Int], y: Int, line_height: Int): Unit = |
43381 | 127 |
{ |
49356 | 128 |
painter_rendering = null |
46220
663251a395c2
more explicit/robust treatment of common snapshot;
wenzelm
parents:
46205
diff
changeset
|
129 |
painter_clip = null |
72900 | 130 |
caret_focus = Rendering.Focus.empty |
43381 | 131 |
} |
132 |
} |
|
133 |
||
73340 | 134 |
def robust_rendering(body: JEdit_Rendering => Unit): Unit = |
46220
663251a395c2
more explicit/robust treatment of common snapshot;
wenzelm
parents:
46205
diff
changeset
|
135 |
{ |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
136 |
robust_body(()) { body(painter_rendering) } |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
137 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
138 |
|
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
139 |
|
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
140 |
/* active areas within the text */ |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
141 |
|
56317
1147854080b4
tuned rendering -- change mouse pointer for active areas;
wenzelm
parents:
56172
diff
changeset
|
142 |
private class Active_Area[A]( |
64621 | 143 |
rendering: JEdit_Rendering => Text.Range => Option[Text.Info[A]], |
56317
1147854080b4
tuned rendering -- change mouse pointer for active areas;
wenzelm
parents:
56172
diff
changeset
|
144 |
cursor: Option[Int]) |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
145 |
{ |
49493
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
146 |
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
|
147 |
|
55688 | 148 |
def is_active: Boolean = the_text_info.isDefined |
49493
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
149 |
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
|
150 |
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
|
151 |
|
73340 | 152 |
def update(new_info: Option[Text.Info[A]]): Unit = |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
153 |
{ |
49493
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
154 |
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
|
155 |
val new_text_info = |
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
156 |
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
|
157 |
|
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
158 |
if (new_text_info != old_text_info) { |
63028 | 159 |
caret_update() |
56317
1147854080b4
tuned rendering -- change mouse pointer for active areas;
wenzelm
parents:
56172
diff
changeset
|
160 |
if (cursor.isDefined) { |
1147854080b4
tuned rendering -- change mouse pointer for active areas;
wenzelm
parents:
56172
diff
changeset
|
161 |
if (new_text_info.isDefined) |
1147854080b4
tuned rendering -- change mouse pointer for active areas;
wenzelm
parents:
56172
diff
changeset
|
162 |
text_area.getPainter.setCursor(Cursor.getPredefinedCursor(cursor.get)) |
1147854080b4
tuned rendering -- change mouse pointer for active areas;
wenzelm
parents:
56172
diff
changeset
|
163 |
else |
56406
0e21270952c3
revert ce37fcb30cf2 for the sake of Mac OS X -- let some event listeners of jEdit reset the cursor;
wenzelm
parents:
56373
diff
changeset
|
164 |
text_area.getPainter.resetCursor() |
56317
1147854080b4
tuned rendering -- change mouse pointer for active areas;
wenzelm
parents:
56172
diff
changeset
|
165 |
} |
49493
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
166 |
for { |
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
167 |
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
|
168 |
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
|
169 |
(_, Text.Info(r1, _)) <- opt |
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
170 |
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
|
171 |
} 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
|
172 |
the_text_info = new_text_info |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
173 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
174 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
175 |
|
73340 | 176 |
def update_rendering(r: JEdit_Rendering, range: Text.Range): Unit = |
177 |
update(rendering(r)(range)) |
|
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
178 |
|
73340 | 179 |
def reset: Unit = update(None) |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
180 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
181 |
|
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56884
diff
changeset
|
182 |
// owned by GUI thread |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
183 |
|
56317
1147854080b4
tuned rendering -- change mouse pointer for active areas;
wenzelm
parents:
56172
diff
changeset
|
184 |
private val highlight_area = |
60892 | 185 |
new Active_Area[Color]( |
71601 | 186 |
(rendering: JEdit_Rendering) => rendering.highlight, None) |
60892 | 187 |
|
52980 | 188 |
private val hyperlink_area = |
66082 | 189 |
new Active_Area[PIDE.editor.Hyperlink]( |
71601 | 190 |
(rendering: JEdit_Rendering) => rendering.hyperlink, Some(Cursor.HAND_CURSOR)) |
60892 | 191 |
|
56317
1147854080b4
tuned rendering -- change mouse pointer for active areas;
wenzelm
parents:
56172
diff
changeset
|
192 |
private val active_area = |
60892 | 193 |
new Active_Area[XML.Elem]( |
71601 | 194 |
(rendering: JEdit_Rendering) => rendering.active, Some(Cursor.DEFAULT_CURSOR)) |
49492 | 195 |
|
196 |
private val active_areas = |
|
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50306
diff
changeset
|
197 |
List((highlight_area, true), (hyperlink_area, true), (active_area, false)) |
50216 | 198 |
def active_reset(): Unit = active_areas.foreach(_._1.reset) |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
199 |
|
62988 | 200 |
private def area_active(): Boolean = |
201 |
active_areas.exists({ case (area, _) => area.is_active }) |
|
202 |
||
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
203 |
private val focus_listener = new FocusAdapter { |
73340 | 204 |
override def focusLost(e: FocusEvent): Unit = { robust_body(()) { active_reset() } } |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
205 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
206 |
|
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
207 |
private val window_listener = new WindowAdapter { |
73340 | 208 |
override def windowIconified(e: WindowEvent): Unit = { robust_body(()) { active_reset() } } |
209 |
override def windowDeactivated(e: WindowEvent): Unit = { robust_body(()) { active_reset() } } |
|
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
210 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
211 |
|
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
212 |
private val mouse_listener = new MouseAdapter { |
73340 | 213 |
override def mouseClicked(e: MouseEvent): Unit = |
214 |
{ |
|
49424 | 215 |
robust_body(()) { |
216 |
hyperlink_area.info match { |
|
56433
db69cb14f7ed
prepare "back" position for Navigator, before following hyperlink;
wenzelm
parents:
56406
diff
changeset
|
217 |
case Some(Text.Info(range, link)) => |
56494
1b74abf064e1
avoid confusion about pointless cursor movement with external links;
wenzelm
parents:
56433
diff
changeset
|
218 |
if (!link.external) { |
1b74abf064e1
avoid confusion about pointless cursor movement with external links;
wenzelm
parents:
56433
diff
changeset
|
219 |
try { text_area.moveCaretPosition(range.start) } |
1b74abf064e1
avoid confusion about pointless cursor movement with external links;
wenzelm
parents:
56433
diff
changeset
|
220 |
catch { |
1b74abf064e1
avoid confusion about pointless cursor movement with external links;
wenzelm
parents:
56433
diff
changeset
|
221 |
case _: ArrayIndexOutOfBoundsException => |
1b74abf064e1
avoid confusion about pointless cursor movement with external links;
wenzelm
parents:
56433
diff
changeset
|
222 |
case _: IllegalArgumentException => |
1b74abf064e1
avoid confusion about pointless cursor movement with external links;
wenzelm
parents:
56433
diff
changeset
|
223 |
} |
73367 | 224 |
text_area.requestFocus() |
56433
db69cb14f7ed
prepare "back" position for Navigator, before following hyperlink;
wenzelm
parents:
56406
diff
changeset
|
225 |
} |
52482
5b7c4fb41511
explicit Pretty_Tooltip.dismiss_all due to slightly changed focus mechanics;
wenzelm
parents:
52480
diff
changeset
|
226 |
link.follow(view) |
49492 | 227 |
case None => |
228 |
} |
|
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50306
diff
changeset
|
229 |
active_area.text_info match { |
50915
12de8ea66f54
close tooltip after Active.action, to make it look more interactive (notably due to lack of dynamic update);
wenzelm
parents:
50849
diff
changeset
|
230 |
case Some((text, Text.Info(_, markup))) => |
12de8ea66f54
close tooltip after Active.action, to make it look more interactive (notably due to lack of dynamic update);
wenzelm
parents:
50849
diff
changeset
|
231 |
Active.action(view, text, markup) |
12de8ea66f54
close tooltip after Active.action, to make it look more interactive (notably due to lack of dynamic update);
wenzelm
parents:
50849
diff
changeset
|
232 |
close_action() |
49424 | 233 |
case None => |
234 |
} |
|
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
235 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
236 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
237 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
238 |
|
56322
f9ad26836516
check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;
wenzelm
parents:
56321
diff
changeset
|
239 |
private def mouse_inside_painter(): Boolean = |
f9ad26836516
check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;
wenzelm
parents:
56321
diff
changeset
|
240 |
MouseInfo.getPointerInfo match { |
f9ad26836516
check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;
wenzelm
parents:
56321
diff
changeset
|
241 |
case null => false |
f9ad26836516
check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;
wenzelm
parents:
56321
diff
changeset
|
242 |
case info => |
f9ad26836516
check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;
wenzelm
parents:
56321
diff
changeset
|
243 |
val point = info.getLocation |
f9ad26836516
check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;
wenzelm
parents:
56321
diff
changeset
|
244 |
val painter = text_area.getPainter |
f9ad26836516
check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;
wenzelm
parents:
56321
diff
changeset
|
245 |
SwingUtilities.convertPointFromScreen(point, painter) |
f9ad26836516
check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;
wenzelm
parents:
56321
diff
changeset
|
246 |
painter.contains(point) |
f9ad26836516
check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;
wenzelm
parents:
56321
diff
changeset
|
247 |
} |
f9ad26836516
check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;
wenzelm
parents:
56321
diff
changeset
|
248 |
|
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
249 |
private val mouse_motion_listener = new MouseMotionAdapter { |
73340 | 250 |
override def mouseDragged(evt: MouseEvent): Unit = |
251 |
{ |
|
56321
7e8c11011fdf
dismiss all popups on mouse drags, e.g. to avoid conflict of C-hover of Isabelle/jEdit and C-selection of jEdit;
wenzelm
parents:
56317
diff
changeset
|
252 |
robust_body(()) { |
57857
4d86378e635f
even more thorough reset on mouse drag (see also 0c63f3538639, 7e8c11011fdf);
wenzelm
parents:
57612
diff
changeset
|
253 |
active_reset() |
56497
0c63f3538639
dismiss popups more carefully (amending 7e8c11011fdf), notably allow mouse dragging within some tooltip, e.g. for text selection;
wenzelm
parents:
56496
diff
changeset
|
254 |
Completion_Popup.Text_Area.dismissed(text_area) |
0c63f3538639
dismiss popups more carefully (amending 7e8c11011fdf), notably allow mouse dragging within some tooltip, e.g. for text selection;
wenzelm
parents:
56496
diff
changeset
|
255 |
Pretty_Tooltip.dismiss_descendant(text_area.getPainter) |
56321
7e8c11011fdf
dismiss all popups on mouse drags, e.g. to avoid conflict of C-hover of Isabelle/jEdit and C-selection of jEdit;
wenzelm
parents:
56317
diff
changeset
|
256 |
} |
7e8c11011fdf
dismiss all popups on mouse drags, e.g. to avoid conflict of C-hover of Isabelle/jEdit and C-selection of jEdit;
wenzelm
parents:
56317
diff
changeset
|
257 |
} |
7e8c11011fdf
dismiss all popups on mouse drags, e.g. to avoid conflict of C-hover of Isabelle/jEdit and C-selection of jEdit;
wenzelm
parents:
56317
diff
changeset
|
258 |
|
73340 | 259 |
override def mouseMoved(evt: MouseEvent): Unit = |
260 |
{ |
|
49424 | 261 |
robust_body(()) { |
53182 | 262 |
val x = evt.getX |
263 |
val y = evt.getY |
|
72899 | 264 |
val control = JEdit_Lib.command_modifier(evt) |
49492 | 265 |
|
53179 | 266 |
if ((control || enable_hovering) && !buffer.isLoading) { |
49424 | 267 |
JEdit_Lib.buffer_lock(buffer) { |
53182 | 268 |
JEdit_Lib.pixel_range(text_area, x, y) match { |
50211 | 269 |
case None => active_reset() |
49941
f2db0596bd61
more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents:
49843
diff
changeset
|
270 |
case Some(range) => |
f2db0596bd61
more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents:
49843
diff
changeset
|
271 |
val rendering = get_rendering() |
f2db0596bd61
more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents:
49843
diff
changeset
|
272 |
for ((area, require_control) <- active_areas) |
f2db0596bd61
more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents:
49843
diff
changeset
|
273 |
{ |
50165
24d47733975f
reset active area for outdated snapshot (again?);
wenzelm
parents:
50164
diff
changeset
|
274 |
if (control == require_control && !rendering.snapshot.is_outdated) |
49941
f2db0596bd61
more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents:
49843
diff
changeset
|
275 |
area.update_rendering(rendering, range) |
f2db0596bd61
more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents:
49843
diff
changeset
|
276 |
else area.reset |
f2db0596bd61
more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents:
49843
diff
changeset
|
277 |
} |
49492 | 278 |
} |
49424 | 279 |
} |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
280 |
} |
49424 | 281 |
else active_reset() |
51441
37f699750430
more elementary tooltips via mouse events (imitating parts of javax.swing.ToolTipManager) -- avoid abuse of getToolTipText to produce window as side-effect;
wenzelm
parents:
50915
diff
changeset
|
282 |
|
53182 | 283 |
if (evt.getSource == text_area.getPainter) { |
52494
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52483
diff
changeset
|
284 |
Pretty_Tooltip.invoke(() => |
52495 | 285 |
robust_body(()) { |
56322
f9ad26836516
check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;
wenzelm
parents:
56321
diff
changeset
|
286 |
if (mouse_inside_painter()) { |
f9ad26836516
check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;
wenzelm
parents:
56321
diff
changeset
|
287 |
val rendering = get_rendering() |
f9ad26836516
check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;
wenzelm
parents:
56321
diff
changeset
|
288 |
val snapshot = rendering.snapshot |
f9ad26836516
check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;
wenzelm
parents:
56321
diff
changeset
|
289 |
if (!snapshot.is_outdated) { |
f9ad26836516
check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;
wenzelm
parents:
56321
diff
changeset
|
290 |
JEdit_Lib.pixel_range(text_area, x, y) match { |
f9ad26836516
check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;
wenzelm
parents:
56321
diff
changeset
|
291 |
case None => |
f9ad26836516
check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;
wenzelm
parents:
56321
diff
changeset
|
292 |
case Some(range) => |
71496 | 293 |
rendering.tooltip(range, control) match { |
56322
f9ad26836516
check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;
wenzelm
parents:
56321
diff
changeset
|
294 |
case None => |
f9ad26836516
check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;
wenzelm
parents:
56321
diff
changeset
|
295 |
case Some(tip) => |
f9ad26836516
check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;
wenzelm
parents:
56321
diff
changeset
|
296 |
val painter = text_area.getPainter |
58767
30766b5fd0e1
proper line height and text base line, like regular TextAreaPainter.PaintText;
wenzelm
parents:
57857
diff
changeset
|
297 |
val loc = new Point(x, y + painter.getLineHeight / 2) |
65332 | 298 |
val results = snapshot.command_results(tip.range) |
56322
f9ad26836516
check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;
wenzelm
parents:
56321
diff
changeset
|
299 |
Pretty_Tooltip(view, painter, loc, rendering, results, tip) |
f9ad26836516
check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;
wenzelm
parents:
56321
diff
changeset
|
300 |
} |
f9ad26836516
check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;
wenzelm
parents:
56321
diff
changeset
|
301 |
} |
52494
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52483
diff
changeset
|
302 |
} |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52483
diff
changeset
|
303 |
} |
52495 | 304 |
}) |
51452
14e6d761ba1c
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents:
51449
diff
changeset
|
305 |
} |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
306 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
307 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
308 |
} |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
309 |
|
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
310 |
|
55713
734ac5709fbe
clarified painting of invisible caret, e.g. focus change due to popup;
wenzelm
parents:
55711
diff
changeset
|
311 |
/* text background */ |
734ac5709fbe
clarified painting of invisible caret, e.g. focus change due to popup;
wenzelm
parents:
55711
diff
changeset
|
312 |
|
43381 | 313 |
private val background_painter = new TextAreaExtension |
314 |
{ |
|
315 |
override def paintScreenLineRange(gfx: Graphics2D, |
|
316 |
first_line: Int, last_line: Int, physical_lines: Array[Int], |
|
73340 | 317 |
start: Array[Int], end: Array[Int], y: Int, line_height: Int): Unit = |
43381 | 318 |
{ |
49356 | 319 |
robust_rendering { rendering => |
51581
587c917e8d36
paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents:
51577
diff
changeset
|
320 |
val fm = text_area.getPainter.getFontMetrics |
43376
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
321 |
|
71601 | 322 |
for (i <- physical_lines.indices) { |
43381 | 323 |
if (physical_lines(i) != -1) { |
56884
7de69b35bdaf
more robust line_range, according to usual jEdit confusion at end of last line (see also 71c5d1f516c0);
wenzelm
parents:
56883
diff
changeset
|
324 |
val line_range = Text.Range(start(i), end(i) min buffer.getLength) |
43376
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
325 |
|
49473 | 326 |
// line background color |
65124 | 327 |
for { (c, separator) <- rendering.line_background(line_range) } |
49473 | 328 |
{ |
65124 | 329 |
gfx.setColor(rendering.color(c)) |
60215 | 330 |
val sep = if (separator) 2 min (line_height / 2) else 0 |
49475 | 331 |
gfx.fillRect(0, y + i * line_height, text_area.getWidth, line_height - sep) |
49473 | 332 |
} |
333 |
||
55790
4670f18baba5
simplified rendering -- no need to over-emphasize "token_range";
wenzelm
parents:
55766
diff
changeset
|
334 |
// background color |
43381 | 335 |
for { |
65176 | 336 |
Text.Info(range, c) <- |
337 |
rendering.background(Rendering.background_elements, line_range, caret_focus) |
|
49409 | 338 |
r <- JEdit_Lib.gfx_range(text_area, range) |
43381 | 339 |
} { |
65101 | 340 |
gfx.setColor(rendering.color(c)) |
43381 | 341 |
gfx.fillRect(r.x, y + i * line_height, r.length, line_height) |
342 |
} |
|
43376
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
343 |
|
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50306
diff
changeset
|
344 |
// active area -- potentially from other snapshot |
49492 | 345 |
for { |
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50306
diff
changeset
|
346 |
info <- active_area.info |
49492 | 347 |
Text.Info(range, _) <- info.try_restrict(line_range) |
348 |
r <- JEdit_Lib.gfx_range(text_area, range) |
|
349 |
} { |
|
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50306
diff
changeset
|
350 |
gfx.setColor(rendering.active_hover_color) |
49492 | 351 |
gfx.fillRect(r.x, y + i * line_height, r.length, line_height) |
352 |
} |
|
353 |
||
43381 | 354 |
// squiggly underline |
355 |
for { |
|
65121 | 356 |
Text.Info(range, c) <- rendering.squiggly_underline(line_range) |
49409 | 357 |
r <- JEdit_Lib.gfx_range(text_area, range) |
43381 | 358 |
} { |
65121 | 359 |
gfx.setColor(rendering.color(c)) |
43381 | 360 |
val x0 = (r.x / 2) * 2 |
51574
2b58d7b139d6
ghost bullet via markup, which is painted as bar under text (normally space);
wenzelm
parents:
51496
diff
changeset
|
361 |
val y0 = r.y + fm.getAscent + 1 |
43381 | 362 |
for (x1 <- Range(x0, x0 + r.length, 2)) { |
363 |
val y1 = if (x1 % 4 < 2) y0 else y0 + 1 |
|
364 |
gfx.drawLine(x1, y1, x1 + 1, y1) |
|
43376
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
365 |
} |
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
366 |
} |
56550 | 367 |
|
56560
ac916ea744e4
tuned rendering -- avoid overlap with squiggly underline;
wenzelm
parents:
56558
diff
changeset
|
368 |
// spell checker |
56550 | 369 |
for { |
65239
509a9b0ad02e
avoid global variables with implicit initialization;
wenzelm
parents:
65213
diff
changeset
|
370 |
spell_checker <- PIDE.plugin.spell_checker.get |
67395
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67014
diff
changeset
|
371 |
spell <- rendering.spell_checker(line_range) |
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67014
diff
changeset
|
372 |
text <- JEdit_Lib.get_text(buffer, spell.range) |
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67014
diff
changeset
|
373 |
info <- spell_checker.marked_words(spell.range.start, text) |
56565 | 374 |
r <- JEdit_Lib.gfx_range(text_area, info.range) |
56550 | 375 |
} { |
376 |
gfx.setColor(rendering.spell_checker_color) |
|
56560
ac916ea744e4
tuned rendering -- avoid overlap with squiggly underline;
wenzelm
parents:
56558
diff
changeset
|
377 |
val y0 = r.y + ((fm.getAscent + 4) min (line_height - 2)) |
56550 | 378 |
gfx.drawLine(r.x, y0, r.x + r.length, y0) |
379 |
} |
|
43376
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
380 |
} |
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
381 |
} |
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43375
diff
changeset
|
382 |
} |
43381 | 383 |
} |
384 |
} |
|
385 |
||
386 |
||
387 |
/* text */ |
|
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
388 |
|
55766 | 389 |
private def caret_enabled: Boolean = |
390 |
caret_visible && (!text_area.hasFocus || text_area.isCaretVisible) |
|
391 |
||
64621 | 392 |
private def caret_color(rendering: JEdit_Rendering, offset: Text.Offset): Color = |
55747
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55726
diff
changeset
|
393 |
{ |
61011 | 394 |
if (text_area.isCaretVisible) text_area.getPainter.getCaretColor |
61014 | 395 |
else { |
396 |
val debug_positions = |
|
61017 | 397 |
(for { |
65247 | 398 |
c <- PIDE.session.debugger.focus().iterator |
61017 | 399 |
pos <- c.debug_position.iterator |
400 |
} yield pos).toList |
|
66082 | 401 |
if (debug_positions.exists(PIDE.editor.is_hyperlink_position(rendering.snapshot, offset, _))) |
61011 | 402 |
rendering.caret_debugger_color |
403 |
else rendering.caret_invisible_color |
|
61014 | 404 |
} |
55747
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55726
diff
changeset
|
405 |
} |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55726
diff
changeset
|
406 |
|
64621 | 407 |
private def paint_chunk_list(rendering: JEdit_Rendering, |
43505 | 408 |
gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float = |
43382 | 409 |
{ |
410 |
val clip_rect = gfx.getClipBounds |
|
55747
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55726
diff
changeset
|
411 |
|
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55726
diff
changeset
|
412 |
val caret_range = |
56592
5157f7615e99
prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents:
56565
diff
changeset
|
413 |
if (caret_enabled) JEdit_Lib.caret_range(text_area) |
56172 | 414 |
else Text.Range.offside |
43382 | 415 |
|
416 |
var w = 0.0f |
|
417 |
var chunk = head |
|
418 |
while (chunk != null) { |
|
43505 | 419 |
val chunk_offset = line_start + chunk.offset |
43382 | 420 |
if (x + w + chunk.width > clip_rect.x && |
50306 | 421 |
x + w < clip_rect.x + clip_rect.width && chunk.length > 0) |
43382 | 422 |
{ |
43505 | 423 |
val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length) |
71932
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
71783
diff
changeset
|
424 |
val chunk_str = |
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
71783
diff
changeset
|
425 |
if (chunk.chars == null) Symbol.spaces(chunk.length) |
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
71783
diff
changeset
|
426 |
else { |
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
71783
diff
changeset
|
427 |
if (chunk.str == null) { chunk.str = new String(chunk.chars) } |
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
71783
diff
changeset
|
428 |
chunk.str |
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
71783
diff
changeset
|
429 |
} |
43382 | 430 |
val chunk_font = chunk.style.getFont |
431 |
val chunk_color = chunk.style.getForegroundColor |
|
432 |
||
73875
6e43936f2111
more ambitious use of AttributedString (despite be825a69fc67, which was for much older Java);
wenzelm
parents:
73367
diff
changeset
|
433 |
val chunk_text = new AttributedString(chunk_str) |
44056
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
434 |
|
73875
6e43936f2111
more ambitious use of AttributedString (despite be825a69fc67, which was for much older Java);
wenzelm
parents:
73367
diff
changeset
|
435 |
def chunk_attrib(attrib: TextAttribute, value: AnyRef, r: Text.Range): Unit = |
6e43936f2111
more ambitious use of AttributedString (despite be825a69fc67, which was for much older Java);
wenzelm
parents:
73367
diff
changeset
|
436 |
chunk_text.addAttribute(attrib, value, r.start - chunk_offset, r.stop - chunk_offset) |
43382 | 437 |
|
73875
6e43936f2111
more ambitious use of AttributedString (despite be825a69fc67, which was for much older Java);
wenzelm
parents:
73367
diff
changeset
|
438 |
// font |
73877 | 439 |
chunk_text.addAttribute(TextAttribute.RUN_DIRECTION, TextAttribute.RUN_DIRECTION_LTR) |
73875
6e43936f2111
more ambitious use of AttributedString (despite be825a69fc67, which was for much older Java);
wenzelm
parents:
73367
diff
changeset
|
440 |
chunk_text.addAttribute(TextAttribute.FONT, chunk_font) |
73876 | 441 |
if (chunk.usedFontSubstitution) { |
442 |
for { |
|
443 |
(c, i) <- Codepoint.iterator_offset(chunk_str) if !chunk_font.canDisplay(c) |
|
444 |
subst_font = Chunk.getSubstFont(c) if subst_font != null |
|
445 |
} { |
|
446 |
val r = Text.Range(i, i + Character.charCount(c)) + chunk_offset |
|
447 |
val font = Chunk.deriveSubstFont(chunk_font, subst_font) |
|
448 |
chunk_attrib(TextAttribute.FONT, font, r) |
|
449 |
} |
|
450 |
} |
|
43448
90aec5043461
more robust caret painting wrt. surrogate characters;
wenzelm
parents:
43435
diff
changeset
|
451 |
|
73875
6e43936f2111
more ambitious use of AttributedString (despite be825a69fc67, which was for much older Java);
wenzelm
parents:
73367
diff
changeset
|
452 |
// color |
6e43936f2111
more ambitious use of AttributedString (despite be825a69fc67, which was for much older Java);
wenzelm
parents:
73367
diff
changeset
|
453 |
chunk_text.addAttribute(TextAttribute.FOREGROUND, chunk_color) |
6e43936f2111
more ambitious use of AttributedString (despite be825a69fc67, which was for much older Java);
wenzelm
parents:
73367
diff
changeset
|
454 |
for { |
6e43936f2111
more ambitious use of AttributedString (despite be825a69fc67, which was for much older Java);
wenzelm
parents:
73367
diff
changeset
|
455 |
Text.Info(r1, color) <- rendering.text_color(chunk_range, chunk_color).iterator |
6e43936f2111
more ambitious use of AttributedString (despite be825a69fc67, which was for much older Java);
wenzelm
parents:
73367
diff
changeset
|
456 |
r2 <- r1.try_restrict(chunk_range) if !r2.is_singularity |
6e43936f2111
more ambitious use of AttributedString (despite be825a69fc67, which was for much older Java);
wenzelm
parents:
73367
diff
changeset
|
457 |
} chunk_attrib(TextAttribute.FOREGROUND, color, r2) |
44056
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
458 |
|
73875
6e43936f2111
more ambitious use of AttributedString (despite be825a69fc67, which was for much older Java);
wenzelm
parents:
73367
diff
changeset
|
459 |
// caret |
6e43936f2111
more ambitious use of AttributedString (despite be825a69fc67, which was for much older Java);
wenzelm
parents:
73367
diff
changeset
|
460 |
for { r <- caret_range.try_restrict(chunk_range) if !r.is_singularity } { |
6e43936f2111
more ambitious use of AttributedString (despite be825a69fc67, which was for much older Java);
wenzelm
parents:
73367
diff
changeset
|
461 |
chunk_attrib(TextAttribute.FOREGROUND, caret_color(rendering, r.start), r) |
6e43936f2111
more ambitious use of AttributedString (despite be825a69fc67, which was for much older Java);
wenzelm
parents:
73367
diff
changeset
|
462 |
chunk_attrib(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, r) |
6e43936f2111
more ambitious use of AttributedString (despite be825a69fc67, which was for much older Java);
wenzelm
parents:
73367
diff
changeset
|
463 |
} |
44056
be825a69fc67
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents:
43759
diff
changeset
|
464 |
|
73875
6e43936f2111
more ambitious use of AttributedString (despite be825a69fc67, which was for much older Java);
wenzelm
parents:
73367
diff
changeset
|
465 |
gfx.drawString(chunk_text.getIterator, x + w, y) |
43382 | 466 |
} |
467 |
w += chunk.width |
|
468 |
chunk = chunk.next.asInstanceOf[Chunk] |
|
469 |
} |
|
470 |
w |
|
471 |
} |
|
472 |
||
43381 | 473 |
private val text_painter = new TextAreaExtension |
474 |
{ |
|
475 |
override def paintScreenLineRange(gfx: Graphics2D, |
|
476 |
first_line: Int, last_line: Int, physical_lines: Array[Int], |
|
73340 | 477 |
start: Array[Int], end: Array[Int], y: Int, line_height: Int): Unit = |
43381 | 478 |
{ |
49356 | 479 |
robust_rendering { rendering => |
51581
587c917e8d36
paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents:
51577
diff
changeset
|
480 |
val painter = text_area.getPainter |
587c917e8d36
paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents:
51577
diff
changeset
|
481 |
val fm = painter.getFontMetrics |
587c917e8d36
paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents:
51577
diff
changeset
|
482 |
val lm = painter.getFont.getLineMetrics(" ", painter.getFontRenderContext) |
587c917e8d36
paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents:
51577
diff
changeset
|
483 |
|
43381 | 484 |
val clip = gfx.getClip |
485 |
val x0 = text_area.getHorizontalOffset |
|
58767
30766b5fd0e1
proper line height and text base line, like regular TextAreaPainter.PaintText;
wenzelm
parents:
57857
diff
changeset
|
486 |
var y0 = y + painter.getLineHeight - (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
|
487 |
|
51581
587c917e8d36
paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents:
51577
diff
changeset
|
488 |
val (bullet_x, bullet_y, bullet_w, bullet_h) = |
587c917e8d36
paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents:
51577
diff
changeset
|
489 |
{ |
587c917e8d36
paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents:
51577
diff
changeset
|
490 |
val w = fm.charWidth(' ') |
587c917e8d36
paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents:
51577
diff
changeset
|
491 |
val b = (w / 2) max 1 |
587c917e8d36
paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents:
51577
diff
changeset
|
492 |
val c = (lm.getAscent + lm.getStrikethroughOffset).round.toInt |
587c917e8d36
paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents:
51577
diff
changeset
|
493 |
((w - b + 1) / 2, c - b / 2, w - b, line_height - b) |
587c917e8d36
paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents:
51577
diff
changeset
|
494 |
} |
587c917e8d36
paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents:
51577
diff
changeset
|
495 |
|
71601 | 496 |
for (i <- physical_lines.indices) { |
49097
4e5e48c589ea
more direct access to all-important chunks for text painting;
wenzelm
parents:
48921
diff
changeset
|
497 |
val line = physical_lines(i) |
4e5e48c589ea
more direct access to all-important chunks for text painting;
wenzelm
parents:
48921
diff
changeset
|
498 |
if (line != -1) { |
56884
7de69b35bdaf
more robust line_range, according to usual jEdit confusion at end of last line (see also 71c5d1f516c0);
wenzelm
parents:
56883
diff
changeset
|
499 |
val line_range = Text.Range(start(i), end(i) min buffer.getLength) |
51581
587c917e8d36
paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents:
51577
diff
changeset
|
500 |
|
587c917e8d36
paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents:
51577
diff
changeset
|
501 |
// text chunks |
49097
4e5e48c589ea
more direct access to all-important chunks for text painting;
wenzelm
parents:
48921
diff
changeset
|
502 |
val screen_line = first_line + i |
4e5e48c589ea
more direct access to all-important chunks for text painting;
wenzelm
parents:
48921
diff
changeset
|
503 |
val chunks = text_area.getChunksOfScreenLine(screen_line) |
4e5e48c589ea
more direct access to all-important chunks for text painting;
wenzelm
parents:
48921
diff
changeset
|
504 |
if (chunks != null) { |
56358
ed09e5f3aedf
more uniform painting of caret, which also improves visibility in invisible state;
wenzelm
parents:
56340
diff
changeset
|
505 |
try { |
ed09e5f3aedf
more uniform painting of caret, which also improves visibility in invisible state;
wenzelm
parents:
56340
diff
changeset
|
506 |
val line_start = buffer.getLineStartOffset(line) |
ed09e5f3aedf
more uniform painting of caret, which also improves visibility in invisible state;
wenzelm
parents:
56340
diff
changeset
|
507 |
gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height) |
73343
d0378baf7d06
tuned --- avoid deprecated conversions between certain number type;
wenzelm
parents:
73340
diff
changeset
|
508 |
val w = |
d0378baf7d06
tuned --- avoid deprecated conversions between certain number type;
wenzelm
parents:
73340
diff
changeset
|
509 |
paint_chunk_list(rendering, gfx, line_start, chunks, x0.toFloat, y0.toFloat).toInt |
56358
ed09e5f3aedf
more uniform painting of caret, which also improves visibility in invisible state;
wenzelm
parents:
56340
diff
changeset
|
510 |
gfx.clipRect(x0 + w.toInt, 0, Integer.MAX_VALUE, Integer.MAX_VALUE) |
ed09e5f3aedf
more uniform painting of caret, which also improves visibility in invisible state;
wenzelm
parents:
56340
diff
changeset
|
511 |
orig_text_painter.paintValidLine(gfx, |
ed09e5f3aedf
more uniform painting of caret, which also improves visibility in invisible state;
wenzelm
parents:
56340
diff
changeset
|
512 |
screen_line, line, start(i), end(i), y + line_height * i) |
ed09e5f3aedf
more uniform painting of caret, which also improves visibility in invisible state;
wenzelm
parents:
56340
diff
changeset
|
513 |
} finally { gfx.setClip(clip) } |
49097
4e5e48c589ea
more direct access to all-important chunks for text painting;
wenzelm
parents:
48921
diff
changeset
|
514 |
} |
60913 | 515 |
|
516 |
// bullet bar |
|
517 |
for { |
|
518 |
Text.Info(range, color) <- rendering.bullet(line_range) |
|
519 |
r <- JEdit_Lib.gfx_range(text_area, range) |
|
520 |
} { |
|
521 |
gfx.setColor(color) |
|
522 |
gfx.fillRect(r.x + bullet_x, y + i * line_height + bullet_y, |
|
523 |
r.length - bullet_w, line_height - bullet_h) |
|
524 |
} |
|
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
525 |
} |
43381 | 526 |
y0 += line_height |
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
527 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
528 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
529 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
530 |
} |
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 |
|
43435
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
533 |
/* foreground */ |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
534 |
|
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
535 |
private val foreground_painter = new TextAreaExtension |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
536 |
{ |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
537 |
override def paintScreenLineRange(gfx: Graphics2D, |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
538 |
first_line: Int, last_line: Int, physical_lines: Array[Int], |
73340 | 539 |
start: Array[Int], end: Array[Int], y: Int, line_height: Int): Unit = |
43435
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
540 |
{ |
49356 | 541 |
robust_rendering { rendering => |
56883
38c6b70e5e53
common support for search field, which is actually a light-weight Highlighter;
wenzelm
parents:
56662
diff
changeset
|
542 |
val search_pattern = get_search_pattern() |
71601 | 543 |
for (i <- physical_lines.indices) { |
43435
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
544 |
if (physical_lines(i) != -1) { |
56884
7de69b35bdaf
more robust line_range, according to usual jEdit confusion at end of last line (see also 71c5d1f516c0);
wenzelm
parents:
56883
diff
changeset
|
545 |
val line_range = Text.Range(start(i), end(i) min buffer.getLength) |
43435
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
546 |
|
44545
3c40007aa031
transparent foreground color for quoted entities;
wenzelm
parents:
44056
diff
changeset
|
547 |
// foreground color |
3c40007aa031
transparent foreground color for quoted entities;
wenzelm
parents:
44056
diff
changeset
|
548 |
for { |
65101 | 549 |
Text.Info(range, c) <- rendering.foreground(line_range) |
49409 | 550 |
r <- JEdit_Lib.gfx_range(text_area, range) |
44545
3c40007aa031
transparent foreground color for quoted entities;
wenzelm
parents:
44056
diff
changeset
|
551 |
} { |
65101 | 552 |
gfx.setColor(rendering.color(c)) |
44545
3c40007aa031
transparent foreground color for quoted entities;
wenzelm
parents:
44056
diff
changeset
|
553 |
gfx.fillRect(r.x, y + i * line_height, r.length, line_height) |
3c40007aa031
transparent foreground color for quoted entities;
wenzelm
parents:
44056
diff
changeset
|
554 |
} |
3c40007aa031
transparent foreground color for quoted entities;
wenzelm
parents:
44056
diff
changeset
|
555 |
|
56883
38c6b70e5e53
common support for search field, which is actually a light-weight Highlighter;
wenzelm
parents:
56662
diff
changeset
|
556 |
// search pattern |
38c6b70e5e53
common support for search field, which is actually a light-weight Highlighter;
wenzelm
parents:
56662
diff
changeset
|
557 |
for { |
38c6b70e5e53
common support for search field, which is actually a light-weight Highlighter;
wenzelm
parents:
56662
diff
changeset
|
558 |
regex <- search_pattern |
67014 | 559 |
text <- JEdit_Lib.get_text(buffer, line_range) |
56883
38c6b70e5e53
common support for search field, which is actually a light-weight Highlighter;
wenzelm
parents:
56662
diff
changeset
|
560 |
m <- regex.findAllMatchIn(text) |
38c6b70e5e53
common support for search field, which is actually a light-weight Highlighter;
wenzelm
parents:
56662
diff
changeset
|
561 |
range = Text.Range(m.start, m.end) + line_range.start |
38c6b70e5e53
common support for search field, which is actually a light-weight Highlighter;
wenzelm
parents:
56662
diff
changeset
|
562 |
r <- JEdit_Lib.gfx_range(text_area, range) |
38c6b70e5e53
common support for search field, which is actually a light-weight Highlighter;
wenzelm
parents:
56662
diff
changeset
|
563 |
} { |
38c6b70e5e53
common support for search field, which is actually a light-weight Highlighter;
wenzelm
parents:
56662
diff
changeset
|
564 |
gfx.setColor(rendering.search_color) |
38c6b70e5e53
common support for search field, which is actually a light-weight Highlighter;
wenzelm
parents:
56662
diff
changeset
|
565 |
gfx.fillRect(r.x, y + i * line_height, r.length, line_height) |
38c6b70e5e53
common support for search field, which is actually a light-weight Highlighter;
wenzelm
parents:
56662
diff
changeset
|
566 |
} |
38c6b70e5e53
common support for search field, which is actually a light-weight Highlighter;
wenzelm
parents:
56662
diff
changeset
|
567 |
|
49357 | 568 |
// highlight range -- potentially from other snapshot |
46205 | 569 |
for { |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
570 |
info <- highlight_area.info |
46205 | 571 |
Text.Info(range, color) <- info.try_restrict(line_range) |
49409 | 572 |
r <- JEdit_Lib.gfx_range(text_area, range) |
46205 | 573 |
} { |
574 |
gfx.setColor(color) |
|
575 |
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
|
576 |
} |
48921
5d8d409b897e
support for direct hyperlinks, without the Hyperlinks plugin;
wenzelm
parents:
47471
diff
changeset
|
577 |
|
5d8d409b897e
support for direct hyperlinks, without the Hyperlinks plugin;
wenzelm
parents:
47471
diff
changeset
|
578 |
// hyperlink range -- potentially from other snapshot |
5d8d409b897e
support for direct hyperlinks, without the Hyperlinks plugin;
wenzelm
parents:
47471
diff
changeset
|
579 |
for { |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
580 |
info <- hyperlink_area.info |
48921
5d8d409b897e
support for direct hyperlinks, without the Hyperlinks plugin;
wenzelm
parents:
47471
diff
changeset
|
581 |
Text.Info(range, _) <- info.try_restrict(line_range) |
49409 | 582 |
r <- JEdit_Lib.gfx_range(text_area, range) |
48921
5d8d409b897e
support for direct hyperlinks, without the Hyperlinks plugin;
wenzelm
parents:
47471
diff
changeset
|
583 |
} { |
49356 | 584 |
gfx.setColor(rendering.hyperlink_color) |
48921
5d8d409b897e
support for direct hyperlinks, without the Hyperlinks plugin;
wenzelm
parents:
47471
diff
changeset
|
585 |
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
|
586 |
} |
55688 | 587 |
|
62988 | 588 |
// entity def range |
589 |
if (!area_active() && caret_visible) { |
|
590 |
for { |
|
62991 | 591 |
Text.Info(range, color) <- rendering.entity_ref(line_range, caret_focus) |
62988 | 592 |
r <- JEdit_Lib.gfx_range(text_area, range) |
593 |
} { |
|
594 |
gfx.setColor(color) |
|
595 |
gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1) |
|
596 |
} |
|
597 |
} |
|
598 |
||
55688 | 599 |
// completion range |
62988 | 600 |
if (!area_active() && caret_visible) { |
55747
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55726
diff
changeset
|
601 |
for { |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55726
diff
changeset
|
602 |
completion <- Completion_Popup.Text_Area(text_area) |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55726
diff
changeset
|
603 |
Text.Info(range, color) <- completion.rendering(rendering, line_range) |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55726
diff
changeset
|
604 |
r <- JEdit_Lib.gfx_range(text_area, range) |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55726
diff
changeset
|
605 |
} { |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55726
diff
changeset
|
606 |
gfx.setColor(color) |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55726
diff
changeset
|
607 |
gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1) |
55711 | 608 |
} |
55688 | 609 |
} |
43435
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
610 |
} |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
611 |
} |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
612 |
} |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
613 |
} |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
614 |
} |
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
615 |
|
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
616 |
|
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
617 |
/* 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
|
618 |
|
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
619 |
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
|
620 |
{ |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
621 |
override def paintValidLine(gfx: Graphics2D, |
73340 | 622 |
screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int): Unit = |
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
623 |
{ |
49356 | 624 |
robust_rendering { _ => |
43404 | 625 |
if (before) gfx.clipRect(0, 0, 0, 0) |
626 |
else gfx.setClip(painter_clip) |
|
627 |
} |
|
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
628 |
} |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
629 |
} |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
630 |
|
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
631 |
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
|
632 |
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
|
633 |
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
|
634 |
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
|
635 |
|
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
636 |
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
|
637 |
{ |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
638 |
override def paintValidLine(gfx: Graphics2D, |
73340 | 639 |
screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int): Unit = |
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
640 |
{ |
55713
734ac5709fbe
clarified painting of invisible caret, e.g. focus change due to popup;
wenzelm
parents:
55711
diff
changeset
|
641 |
robust_rendering { rendering => |
734ac5709fbe
clarified painting of invisible caret, e.g. focus change due to popup;
wenzelm
parents:
55711
diff
changeset
|
642 |
if (caret_visible) { |
43398
c3e2a361b418
more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
wenzelm
parents:
43396
diff
changeset
|
643 |
val caret = text_area.getCaretPosition |
55766 | 644 |
if (caret_enabled && start <= caret && caret == end - 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
|
645 |
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
|
646 |
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
|
647 |
|
43398
c3e2a361b418
more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
wenzelm
parents:
43396
diff
changeset
|
648 |
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
|
649 |
val x = text_area.offsetToXY(physical_line, offset).x |
58767
30766b5fd0e1
proper line height and text base line, like regular TextAreaPainter.PaintText;
wenzelm
parents:
57857
diff
changeset
|
650 |
val y1 = y + painter.getLineHeight - (fm.getLeading + 1) - fm.getDescent |
56358
ed09e5f3aedf
more uniform painting of caret, which also improves visibility in invisible state;
wenzelm
parents:
56340
diff
changeset
|
651 |
|
ed09e5f3aedf
more uniform painting of caret, which also improves visibility in invisible state;
wenzelm
parents:
56340
diff
changeset
|
652 |
val astr = new AttributedString(" ") |
ed09e5f3aedf
more uniform painting of caret, which also improves visibility in invisible state;
wenzelm
parents:
56340
diff
changeset
|
653 |
astr.addAttribute(TextAttribute.FONT, painter.getFont) |
61011 | 654 |
astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering, caret)) |
56358
ed09e5f3aedf
more uniform painting of caret, which also improves visibility in invisible state;
wenzelm
parents:
56340
diff
changeset
|
655 |
astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON) |
ed09e5f3aedf
more uniform painting of caret, which also improves visibility in invisible state;
wenzelm
parents:
56340
diff
changeset
|
656 |
|
ed09e5f3aedf
more uniform painting of caret, which also improves visibility in invisible state;
wenzelm
parents:
56340
diff
changeset
|
657 |
val clip = gfx.getClip |
ed09e5f3aedf
more uniform painting of caret, which also improves visibility in invisible state;
wenzelm
parents:
56340
diff
changeset
|
658 |
try { |
ed09e5f3aedf
more uniform painting of caret, which also improves visibility in invisible state;
wenzelm
parents:
56340
diff
changeset
|
659 |
gfx.clipRect(x, y, Integer.MAX_VALUE, painter.getLineHeight) |
ed09e5f3aedf
more uniform painting of caret, which also improves visibility in invisible state;
wenzelm
parents:
56340
diff
changeset
|
660 |
gfx.drawString(astr.getIterator, x, y1) |
ed09e5f3aedf
more uniform painting of caret, which also improves visibility in invisible state;
wenzelm
parents:
56340
diff
changeset
|
661 |
} |
ed09e5f3aedf
more uniform painting of caret, which also improves visibility in invisible state;
wenzelm
parents:
56340
diff
changeset
|
662 |
finally { gfx.setClip(clip) } |
43398
c3e2a361b418
more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
wenzelm
parents:
43396
diff
changeset
|
663 |
} |
43393
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
664 |
} |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
665 |
} |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
666 |
} |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
667 |
} |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
668 |
|
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
669 |
|
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
670 |
/* activation */ |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
671 |
|
73340 | 672 |
def activate(): Unit = |
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
673 |
{ |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
674 |
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
|
675 |
painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state) |
43381 | 676 |
painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter) |
677 |
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
|
678 |
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
|
679 |
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
|
680 |
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
|
681 |
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
|
682 |
painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter) |
43435
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
683 |
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
|
684 |
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
|
685 |
painter.removeExtension(orig_text_painter) |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
686 |
painter.addMouseListener(mouse_listener) |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
687 |
painter.addMouseMotionListener(mouse_motion_listener) |
72927
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
688 |
text_area.addKeyListener(key_listener) |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
689 |
text_area.addFocusListener(focus_listener) |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
690 |
view.addWindowListener(window_listener) |
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
691 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
692 |
|
73340 | 693 |
def deactivate(): Unit = |
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
694 |
{ |
56340
af8cb60b55eb
clear active areas (notably mouse pointer) before changing context (e.g. via hyperlink);
wenzelm
parents:
56339
diff
changeset
|
695 |
active_reset() |
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
696 |
val painter = text_area.getPainter |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
697 |
view.removeWindowListener(window_listener) |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
698 |
text_area.removeFocusListener(focus_listener) |
72927
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72900
diff
changeset
|
699 |
text_area.removeKeyListener(key_listener) |
49410
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
700 |
painter.removeMouseMotionListener(mouse_motion_listener) |
34acbcc33adf
tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents:
49409
diff
changeset
|
701 |
painter.removeMouseListener(mouse_listener) |
43396 | 702 |
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
|
703 |
painter.removeExtension(reset_state) |
43435
ae6b0c3e58a8
highlight via foreground painter, using alpha channel;
wenzelm
parents:
43434
diff
changeset
|
704 |
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
|
705 |
painter.removeExtension(caret_painter) |
f4141da52e92
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents:
43392
diff
changeset
|
706 |
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
|
707 |
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
|
708 |
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
|
709 |
painter.removeExtension(before_caret_painter1) |
43381 | 710 |
painter.removeExtension(text_painter) |
711 |
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
|
712 |
painter.removeExtension(set_state) |
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
713 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
714 |
} |