| author | wenzelm |
| Sat, 24 Aug 2013 17:41:57 +0200 | |
| changeset 53183 | 018d71bee930 |
| parent 53019 | be9e94594b96 |
| child 53226 | 9cf8e2263ca7 |
| permissions | -rw-r--r-- |
| 49406 | 1 |
/* Title: Tools/jEdit/src/jedit_lib.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Misc library functions for jEdit. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle.jedit |
|
8 |
||
9 |
||
10 |
import isabelle._ |
|
11 |
||
| 50658 | 12 |
import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle}
|
| 53019 | 13 |
import javax.swing.{Icon, ImageIcon, JWindow}
|
|
49710
21d88a631fcc
refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents:
49409
diff
changeset
|
14 |
|
|
21d88a631fcc
refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents:
49409
diff
changeset
|
15 |
import scala.annotation.tailrec |
| 49406 | 16 |
|
| 52873 | 17 |
import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities}
|
| 49406 | 18 |
import org.gjt.sp.jedit.buffer.JEditBuffer |
|
51492
eaa1c4cc1106
more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
wenzelm
parents:
51469
diff
changeset
|
19 |
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
|
| 49406 | 20 |
|
21 |
||
22 |
object JEdit_Lib |
|
23 |
{
|
|
|
50554
0493efcc97e9
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents:
50363
diff
changeset
|
24 |
/* bounds within multi-screen environment */ |
|
0493efcc97e9
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents:
50363
diff
changeset
|
25 |
|
|
0493efcc97e9
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents:
50363
diff
changeset
|
26 |
def screen_bounds(screen_point: Point): Rectangle = |
|
0493efcc97e9
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents:
50363
diff
changeset
|
27 |
{
|
|
0493efcc97e9
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents:
50363
diff
changeset
|
28 |
val ge = GraphicsEnvironment.getLocalGraphicsEnvironment |
|
0493efcc97e9
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents:
50363
diff
changeset
|
29 |
(for {
|
|
0493efcc97e9
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents:
50363
diff
changeset
|
30 |
device <- ge.getScreenDevices.iterator |
|
0493efcc97e9
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents:
50363
diff
changeset
|
31 |
config <- device.getConfigurations.iterator |
|
0493efcc97e9
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents:
50363
diff
changeset
|
32 |
bounds = config.getBounds |
|
0493efcc97e9
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents:
50363
diff
changeset
|
33 |
} yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds |
|
0493efcc97e9
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents:
50363
diff
changeset
|
34 |
} |
|
0493efcc97e9
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents:
50363
diff
changeset
|
35 |
|
|
0493efcc97e9
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents:
50363
diff
changeset
|
36 |
|
| 53019 | 37 |
/* window geometry measurement */ |
38 |
||
39 |
private lazy val dummy_window = new JWindow |
|
40 |
||
41 |
final case class Window_Geometry(width: Int, height: Int, inner_width: Int, inner_height: Int) |
|
42 |
{
|
|
43 |
def deco_width: Int = width - inner_width |
|
44 |
def deco_height: Int = height - inner_height |
|
45 |
} |
|
46 |
||
47 |
def window_geometry(outer: Container, inner: Component): Window_Geometry = |
|
48 |
{
|
|
49 |
Swing_Thread.require() |
|
50 |
||
51 |
val old_content = dummy_window.getContentPane |
|
52 |
||
53 |
dummy_window.setContentPane(outer) |
|
54 |
dummy_window.pack |
|
55 |
dummy_window.revalidate |
|
56 |
||
57 |
val geometry = |
|
58 |
Window_Geometry( |
|
59 |
dummy_window.getWidth, dummy_window.getHeight, inner.getWidth, inner.getHeight) |
|
60 |
||
61 |
dummy_window.setContentPane(old_content) |
|
62 |
||
63 |
geometry |
|
64 |
} |
|
65 |
||
66 |
||
| 49712 | 67 |
/* GUI components */ |
68 |
||
69 |
def get_parent(component: Component): Option[Container] = |
|
70 |
component.getParent match {
|
|
71 |
case null => None |
|
72 |
case parent => Some(parent) |
|
73 |
} |
|
74 |
||
75 |
def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
|
|
76 |
private var next_elem = get_parent(component) |
|
77 |
def hasNext(): Boolean = next_elem.isDefined |
|
78 |
def next(): Container = |
|
79 |
next_elem match {
|
|
80 |
case Some(parent) => |
|
81 |
next_elem = get_parent(parent) |
|
82 |
parent |
|
83 |
case None => Iterator.empty.next() |
|
84 |
} |
|
85 |
} |
|
86 |
||
87 |
def parent_window(component: Component): Option[Window] = |
|
|
52478
0a1db0d02628
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
51507
diff
changeset
|
88 |
ancestors(component).collectFirst({ case x: Window => x })
|
|
49710
21d88a631fcc
refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents:
49409
diff
changeset
|
89 |
|
|
21d88a631fcc
refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents:
49409
diff
changeset
|
90 |
|
|
50186
f83cab68c788
recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
wenzelm
parents:
50116
diff
changeset
|
91 |
/* basic tooltips, with multi-line support */ |
|
f83cab68c788
recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
wenzelm
parents:
50116
diff
changeset
|
92 |
|
|
f83cab68c788
recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
wenzelm
parents:
50116
diff
changeset
|
93 |
def wrap_tooltip(text: String): String = |
|
f83cab68c788
recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
wenzelm
parents:
50116
diff
changeset
|
94 |
if (text == "") null |
|
f83cab68c788
recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
wenzelm
parents:
50116
diff
changeset
|
95 |
else "<html><pre>" + HTML.encode(text) + "</pre></html>" |
|
f83cab68c788
recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
wenzelm
parents:
50116
diff
changeset
|
96 |
|
|
f83cab68c788
recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
wenzelm
parents:
50116
diff
changeset
|
97 |
|
| 49406 | 98 |
/* buffers */ |
99 |
||
100 |
def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A = |
|
101 |
Swing_Thread.now { buffer_lock(buffer) { body } }
|
|
102 |
||
103 |
def buffer_text(buffer: JEditBuffer): String = |
|
104 |
buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
|
|
105 |
||
106 |
def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath |
|
107 |
||
108 |
||
|
53003
39da27fc6101
attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents:
52874
diff
changeset
|
109 |
/* focus of main window */ |
|
39da27fc6101
attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents:
52874
diff
changeset
|
110 |
|
|
39da27fc6101
attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents:
52874
diff
changeset
|
111 |
def request_focus_view: Unit = |
|
39da27fc6101
attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents:
52874
diff
changeset
|
112 |
{
|
|
39da27fc6101
attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents:
52874
diff
changeset
|
113 |
jEdit.getActiveView() match {
|
|
39da27fc6101
attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents:
52874
diff
changeset
|
114 |
case null => |
|
39da27fc6101
attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents:
52874
diff
changeset
|
115 |
case view => |
|
39da27fc6101
attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents:
52874
diff
changeset
|
116 |
view.getTextArea match {
|
|
39da27fc6101
attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents:
52874
diff
changeset
|
117 |
case null => |
|
39da27fc6101
attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents:
52874
diff
changeset
|
118 |
case text_area => text_area.requestFocus |
|
39da27fc6101
attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents:
52874
diff
changeset
|
119 |
} |
|
39da27fc6101
attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents:
52874
diff
changeset
|
120 |
} |
|
39da27fc6101
attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents:
52874
diff
changeset
|
121 |
} |
|
39da27fc6101
attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents:
52874
diff
changeset
|
122 |
|
|
39da27fc6101
attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents:
52874
diff
changeset
|
123 |
|
| 49406 | 124 |
/* main jEdit components */ |
125 |
||
126 |
def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator |
|
127 |
||
128 |
def jedit_buffer(name: String): Option[Buffer] = |
|
129 |
jedit_buffers().find(buffer => buffer_name(buffer) == name) |
|
130 |
||
131 |
def jedit_views(): Iterator[View] = jEdit.getViews().iterator |
|
132 |
||
133 |
def jedit_text_areas(view: View): Iterator[JEditTextArea] = |
|
134 |
view.getEditPanes().iterator.map(_.getTextArea) |
|
135 |
||
136 |
def jedit_text_areas(): Iterator[JEditTextArea] = |
|
137 |
jedit_views().flatMap(jedit_text_areas(_)) |
|
138 |
||
139 |
def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] = |
|
140 |
jedit_text_areas().filter(_.getBuffer == buffer) |
|
141 |
||
142 |
def buffer_lock[A](buffer: JEditBuffer)(body: => A): A = |
|
143 |
{
|
|
144 |
try { buffer.readLock(); body }
|
|
145 |
finally { buffer.readUnlock() }
|
|
146 |
} |
|
| 49407 | 147 |
|
|
50195
863b1dfc396c
prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents:
50186
diff
changeset
|
148 |
def buffer_edit[A](buffer: JEditBuffer)(body: => A): A = |
|
863b1dfc396c
prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents:
50186
diff
changeset
|
149 |
{
|
|
863b1dfc396c
prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents:
50186
diff
changeset
|
150 |
try { buffer.beginCompoundEdit(); body }
|
|
863b1dfc396c
prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents:
50186
diff
changeset
|
151 |
finally { buffer.endCompoundEdit() }
|
|
863b1dfc396c
prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents:
50186
diff
changeset
|
152 |
} |
|
863b1dfc396c
prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents:
50186
diff
changeset
|
153 |
|
| 49407 | 154 |
|
| 50215 | 155 |
/* get text */ |
156 |
||
157 |
def try_get_text(buffer: JEditBuffer, range: Text.Range): Option[String] = |
|
158 |
try { Some(buffer.getText(range.start, range.length)) }
|
|
159 |
catch { case _: ArrayIndexOutOfBoundsException => None }
|
|
160 |
||
161 |
||
|
50363
2f8dc9e65401
tuned signature in accordance to document operations;
wenzelm
parents:
50215
diff
changeset
|
162 |
/* buffer range */ |
|
2f8dc9e65401
tuned signature in accordance to document operations;
wenzelm
parents:
50215
diff
changeset
|
163 |
|
|
2f8dc9e65401
tuned signature in accordance to document operations;
wenzelm
parents:
50215
diff
changeset
|
164 |
def buffer_range(buffer: JEditBuffer): Text.Range = |
|
2f8dc9e65401
tuned signature in accordance to document operations;
wenzelm
parents:
50215
diff
changeset
|
165 |
Text.Range(0, (buffer.getLength - 1) max 0) |
|
2f8dc9e65401
tuned signature in accordance to document operations;
wenzelm
parents:
50215
diff
changeset
|
166 |
|
|
2f8dc9e65401
tuned signature in accordance to document operations;
wenzelm
parents:
50215
diff
changeset
|
167 |
|
| 49407 | 168 |
/* point range */ |
169 |
||
170 |
def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range = |
|
171 |
buffer_lock(buffer) {
|
|
172 |
def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0) |
|
173 |
try {
|
|
174 |
val c = text(offset) |
|
175 |
if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1))) |
|
176 |
Text.Range(offset, offset + 2) |
|
177 |
else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1))) |
|
178 |
Text.Range(offset - 1, offset + 1) |
|
179 |
else Text.Range(offset, offset + 1) |
|
180 |
} |
|
181 |
catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
|
|
182 |
} |
|
| 49408 | 183 |
|
184 |
||
185 |
/* visible text range */ |
|
186 |
||
187 |
def visible_range(text_area: TextArea): Option[Text.Range] = |
|
188 |
{
|
|
189 |
val buffer = text_area.getBuffer |
|
190 |
val n = text_area.getVisibleLines |
|
191 |
if (n > 0) {
|
|
192 |
val start = text_area.getScreenLineStartOffset(0) |
|
193 |
val raw_end = text_area.getScreenLineEndOffset(n - 1) |
|
|
49843
afddf4e26fac
further refinement of jEdit line range, avoiding lack of final \n;
wenzelm
parents:
49712
diff
changeset
|
194 |
val end = if (raw_end >= 0) raw_end min buffer.getLength else buffer.getLength |
|
afddf4e26fac
further refinement of jEdit line range, avoiding lack of final \n;
wenzelm
parents:
49712
diff
changeset
|
195 |
Some(Text.Range(start, end)) |
| 49408 | 196 |
} |
197 |
else None |
|
198 |
} |
|
199 |
||
200 |
def invalidate_range(text_area: TextArea, range: Text.Range) |
|
201 |
{
|
|
202 |
val buffer = text_area.getBuffer |
|
203 |
text_area.invalidateLineRange( |
|
204 |
buffer.getLineOfOffset(range.start), |
|
205 |
buffer.getLineOfOffset(range.stop)) |
|
206 |
} |
|
| 49409 | 207 |
|
208 |
||
209 |
/* graphics range */ |
|
210 |
||
| 50115 | 211 |
case class Gfx_Range(val x: Int, val y: Int, val length: Int) |
| 49409 | 212 |
|
|
49843
afddf4e26fac
further refinement of jEdit line range, avoiding lack of final \n;
wenzelm
parents:
49712
diff
changeset
|
213 |
// NB: jEdit always normalizes \r\n and \r to \n |
| 49409 | 214 |
// NB: last line lacks \n |
215 |
def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] = |
|
216 |
{
|
|
| 51507 | 217 |
val metric = pretty_metric(text_area.getPainter) |
|
51492
eaa1c4cc1106
more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
wenzelm
parents:
51469
diff
changeset
|
218 |
val char_width = (metric.unit * metric.average).round.toInt |
| 50849 | 219 |
|
| 49409 | 220 |
val buffer = text_area.getBuffer |
221 |
||
222 |
val end = buffer.getLength |
|
223 |
val stop = range.stop |
|
|
51078
4e1c940b1fb2
more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
wenzelm
parents:
50849
diff
changeset
|
224 |
|
|
4e1c940b1fb2
more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
wenzelm
parents:
50849
diff
changeset
|
225 |
val (p, q, r) = |
|
4e1c940b1fb2
more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
wenzelm
parents:
50849
diff
changeset
|
226 |
try {
|
|
4e1c940b1fb2
more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
wenzelm
parents:
50849
diff
changeset
|
227 |
val p = text_area.offsetToXY(range.start) |
|
4e1c940b1fb2
more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
wenzelm
parents:
50849
diff
changeset
|
228 |
val (q, r) = |
|
4e1c940b1fb2
more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
wenzelm
parents:
50849
diff
changeset
|
229 |
if (stop >= end) (text_area.offsetToXY(end), char_width * (stop - end)) |
|
4e1c940b1fb2
more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
wenzelm
parents:
50849
diff
changeset
|
230 |
else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n") |
|
4e1c940b1fb2
more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
wenzelm
parents:
50849
diff
changeset
|
231 |
(text_area.offsetToXY(stop - 1), char_width) |
|
4e1c940b1fb2
more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
wenzelm
parents:
50849
diff
changeset
|
232 |
else (text_area.offsetToXY(stop), 0) |
|
4e1c940b1fb2
more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
wenzelm
parents:
50849
diff
changeset
|
233 |
(p, q, r) |
|
4e1c940b1fb2
more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
wenzelm
parents:
50849
diff
changeset
|
234 |
} |
|
4e1c940b1fb2
more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
wenzelm
parents:
50849
diff
changeset
|
235 |
catch { case _: ArrayIndexOutOfBoundsException => (null, null, 0) }
|
| 49409 | 236 |
|
237 |
if (p != null && q != null && p.x < q.x + r && p.y == q.y) |
|
| 50115 | 238 |
Some(Gfx_Range(p.x, p.y, q.x + r - p.x)) |
| 49409 | 239 |
else None |
240 |
} |
|
|
49941
f2db0596bd61
more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents:
49843
diff
changeset
|
241 |
|
|
f2db0596bd61
more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents:
49843
diff
changeset
|
242 |
|
|
f2db0596bd61
more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents:
49843
diff
changeset
|
243 |
/* pixel range */ |
|
f2db0596bd61
more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents:
49843
diff
changeset
|
244 |
|
|
f2db0596bd61
more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents:
49843
diff
changeset
|
245 |
def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] = |
|
f2db0596bd61
more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents:
49843
diff
changeset
|
246 |
{
|
|
53183
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset
|
247 |
// coordinates wrt. inner painter component |
|
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset
|
248 |
val painter = text_area.getPainter |
|
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset
|
249 |
if (0 <= x && x < painter.getWidth && 0 <= y && y < painter.getHeight) {
|
|
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset
|
250 |
val offset = text_area.xyToOffset(x, y, false) |
|
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset
|
251 |
if (offset >= 0) {
|
|
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset
|
252 |
val range = point_range(text_area.getBuffer, offset) |
|
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset
|
253 |
gfx_range(text_area, range) match {
|
|
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset
|
254 |
case Some(g) if (g.x <= x && x < g.x + g.length) => Some(range) |
|
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset
|
255 |
case _ => None |
|
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset
|
256 |
} |
|
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset
|
257 |
} |
|
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset
|
258 |
else None |
|
49941
f2db0596bd61
more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents:
49843
diff
changeset
|
259 |
} |
|
53183
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset
|
260 |
else None |
|
49941
f2db0596bd61
more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents:
49843
diff
changeset
|
261 |
} |
|
51492
eaa1c4cc1106
more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
wenzelm
parents:
51469
diff
changeset
|
262 |
|
|
eaa1c4cc1106
more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
wenzelm
parents:
51469
diff
changeset
|
263 |
|
|
eaa1c4cc1106
more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
wenzelm
parents:
51469
diff
changeset
|
264 |
/* pretty text metric */ |
|
eaa1c4cc1106
more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
wenzelm
parents:
51469
diff
changeset
|
265 |
|
| 51507 | 266 |
abstract class Pretty_Metric extends Pretty.Metric |
267 |
{
|
|
268 |
def average: Double |
|
269 |
} |
|
|
51492
eaa1c4cc1106
more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
wenzelm
parents:
51469
diff
changeset
|
270 |
|
| 51507 | 271 |
def pretty_metric(painter: TextAreaPainter): Pretty_Metric = |
272 |
new Pretty_Metric {
|
|
273 |
def string_width(s: String): Double = |
|
274 |
painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth |
|
275 |
||
276 |
val unit = string_width(Pretty.space) |
|
277 |
val average = string_width("mix") / (3 * unit)
|
|
278 |
def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit |
|
|
51492
eaa1c4cc1106
more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
wenzelm
parents:
51469
diff
changeset
|
279 |
} |
| 52873 | 280 |
|
281 |
||
282 |
/* icons */ |
|
283 |
||
284 |
def load_icon(name: String): Icon = |
|
285 |
{
|
|
286 |
val name1 = |
|
287 |
if (name.startsWith("idea-icons/")) {
|
|
288 |
val file = |
|
289 |
Isabelle_System.platform_file_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
|
|
290 |
"jar:" + file + "!/" + name |
|
291 |
} |
|
292 |
else name |
|
293 |
val icon = GUIUtilities.loadIcon(name1) |
|
294 |
if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name)
|
|
295 |
else icon |
|
296 |
} |
|
| 52874 | 297 |
|
298 |
def load_image_icon(name: String): ImageIcon = |
|
299 |
load_icon(name) match {
|
|
300 |
case icon: ImageIcon => icon |
|
301 |
case _ => error("Bad image icon: " + name)
|
|
302 |
} |
|
| 49406 | 303 |
} |
304 |