author  wenzelm 
Thu, 29 Aug 2013 12:38:33 +0200  
changeset 53274  1760c01f1c78 
parent 53247  bd595338ca18 
child 53712  ea51046be71b 
permissions  rwrr 
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 

53247
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

12 
import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle, Dimension} 
53226
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset

13 
import java.awt.event.{KeyEvent, KeyListener} 
53247
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

14 
import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities} 
49710
21d88a631fcc
refer to parent frame  relevant for floating dockables in particular;
wenzelm
parents:
49409
diff
changeset

15 

21d88a631fcc
refer to parent frame  relevant for floating dockables in particular;
wenzelm
parents:
49409
diff
changeset

16 
import scala.annotation.tailrec 
49406  17 

52873  18 
import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities} 
53226
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset

19 
import org.gjt.sp.jedit.gui.KeyEventWorkaround 
49406  20 
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

21 
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter} 
49406  22 

23 

24 
object JEdit_Lib 

25 
{ 

53247
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

26 
/* location within multiscreen environment */ 
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

27 

bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

28 
final case class Screen_Location(point: Point, bounds: Rectangle) 
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

29 
{ 
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

30 
def relative(parent: Component, size: Dimension): Point = 
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

31 
{ 
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

32 
val w = size.width 
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

33 
val h = size.height 
50554
0493efcc97e9
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multiscreen environment;
wenzelm
parents:
50363
diff
changeset

34 

53247
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

35 
val x0 = parent.getLocationOnScreen.x 
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

36 
val y0 = parent.getLocationOnScreen.y 
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

37 
val x1 = x0 + parent.getWidth  w 
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

38 
val y1 = y0 + parent.getHeight  h 
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

39 
val x2 = point.x min (bounds.x + bounds.width  w) 
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

40 
val y2 = point.y min (bounds.y + bounds.height  h) 
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

41 

bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

42 
val location = new Point((x2 min x1) max x0, (y2 min y1) max y0) 
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

43 
SwingUtilities.convertPointFromScreen(location, parent) 
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

44 
location 
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

45 
} 
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

46 
} 
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

47 

bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

48 
def screen_location(component: Component, point: Point): Screen_Location = 
50554
0493efcc97e9
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multiscreen environment;
wenzelm
parents:
50363
diff
changeset

49 
{ 
53247
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

50 
val screen_point = new Point(point.x, point.y) 
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

51 
SwingUtilities.convertPointToScreen(screen_point, component) 
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

52 

50554
0493efcc97e9
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multiscreen environment;
wenzelm
parents:
50363
diff
changeset

53 
val ge = GraphicsEnvironment.getLocalGraphicsEnvironment 
53247
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

54 
val screen_bounds = 
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

55 
(for { 
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

56 
device < ge.getScreenDevices.iterator 
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

57 
config < device.getConfigurations.iterator 
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

58 
bounds = config.getBounds 
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

59 
} yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds 
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

60 

bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset

61 
Screen_Location(screen_point, screen_bounds) 
50554
0493efcc97e9
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multiscreen environment;
wenzelm
parents:
50363
diff
changeset

62 
} 
0493efcc97e9
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multiscreen environment;
wenzelm
parents:
50363
diff
changeset

63 

0493efcc97e9
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multiscreen environment;
wenzelm
parents:
50363
diff
changeset

64 

53019  65 
/* window geometry measurement */ 
66 

67 
private lazy val dummy_window = new JWindow 

68 

69 
final case class Window_Geometry(width: Int, height: Int, inner_width: Int, inner_height: Int) 

70 
{ 

71 
def deco_width: Int = width  inner_width 

72 
def deco_height: Int = height  inner_height 

73 
} 

74 

75 
def window_geometry(outer: Container, inner: Component): Window_Geometry = 

76 
{ 

77 
Swing_Thread.require() 

78 

79 
val old_content = dummy_window.getContentPane 

80 

81 
dummy_window.setContentPane(outer) 

82 
dummy_window.pack 

83 
dummy_window.revalidate 

84 

85 
val geometry = 

86 
Window_Geometry( 

87 
dummy_window.getWidth, dummy_window.getHeight, inner.getWidth, inner.getHeight) 

88 

89 
dummy_window.setContentPane(old_content) 

90 

91 
geometry 

92 
} 

93 

94 

49712  95 
/* GUI components */ 
96 

97 
def get_parent(component: Component): Option[Container] = 

98 
component.getParent match { 

99 
case null => None 

100 
case parent => Some(parent) 

101 
} 

102 

103 
def ancestors(component: Component): Iterator[Container] = new Iterator[Container] { 

104 
private var next_elem = get_parent(component) 

105 
def hasNext(): Boolean = next_elem.isDefined 

106 
def next(): Container = 

107 
next_elem match { 

108 
case Some(parent) => 

109 
next_elem = get_parent(parent) 

110 
parent 

111 
case None => Iterator.empty.next() 

112 
} 

113 
} 

114 

115 
def parent_window(component: Component): Option[Window] = 

52478
0a1db0d02628
manage popup windows via PopupFactory, which prefers lightweight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents:
51507
diff
changeset

116 
ancestors(component).collectFirst({ case x: Window => x }) 
49710
21d88a631fcc
refer to parent frame  relevant for floating dockables in particular;
wenzelm
parents:
49409
diff
changeset

117 

21d88a631fcc
refer to parent frame  relevant for floating dockables in particular;
wenzelm
parents:
49409
diff
changeset

118 

50186
f83cab68c788
recovered some tooltip wrapping from e2762f962042, with multiline support via HTML.encode;
wenzelm
parents:
50116
diff
changeset

119 
/* basic tooltips, with multiline support */ 
f83cab68c788
recovered some tooltip wrapping from e2762f962042, with multiline support via HTML.encode;
wenzelm
parents:
50116
diff
changeset

120 

f83cab68c788
recovered some tooltip wrapping from e2762f962042, with multiline support via HTML.encode;
wenzelm
parents:
50116
diff
changeset

121 
def wrap_tooltip(text: String): String = 
f83cab68c788
recovered some tooltip wrapping from e2762f962042, with multiline support via HTML.encode;
wenzelm
parents:
50116
diff
changeset

122 
if (text == "") null 
f83cab68c788
recovered some tooltip wrapping from e2762f962042, with multiline support via HTML.encode;
wenzelm
parents:
50116
diff
changeset

123 
else "<html><pre>" + HTML.encode(text) + "</pre></html>" 
f83cab68c788
recovered some tooltip wrapping from e2762f962042, with multiline support via HTML.encode;
wenzelm
parents:
50116
diff
changeset

124 

f83cab68c788
recovered some tooltip wrapping from e2762f962042, with multiline support via HTML.encode;
wenzelm
parents:
50116
diff
changeset

125 

49406  126 
/* buffers */ 
127 

128 
def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A = 

129 
Swing_Thread.now { buffer_lock(buffer) { body } } 

130 

131 
def buffer_text(buffer: JEditBuffer): String = 

132 
buffer_lock(buffer) { buffer.getText(0, buffer.getLength) } 

133 

53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53247
diff
changeset

134 
def buffer_mode(buffer: JEditBuffer): String = 
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53247
diff
changeset

135 
{ 
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53247
diff
changeset

136 
val mode = buffer.getMode 
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53247
diff
changeset

137 
if (mode == null) "" 
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53247
diff
changeset

138 
else { 
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53247
diff
changeset

139 
val name = mode.getName 
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53247
diff
changeset

140 
if (name == null) "" else name 
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53247
diff
changeset

141 
} 
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53247
diff
changeset

142 
} 
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53247
diff
changeset

143 

49406  144 
def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath 
145 

146 

147 
/* main jEdit components */ 

148 

149 
def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator 

150 

151 
def jedit_buffer(name: String): Option[Buffer] = 

152 
jedit_buffers().find(buffer => buffer_name(buffer) == name) 

153 

154 
def jedit_views(): Iterator[View] = jEdit.getViews().iterator 

155 

156 
def jedit_text_areas(view: View): Iterator[JEditTextArea] = 

157 
view.getEditPanes().iterator.map(_.getTextArea) 

158 

159 
def jedit_text_areas(): Iterator[JEditTextArea] = 

160 
jedit_views().flatMap(jedit_text_areas(_)) 

161 

162 
def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] = 

163 
jedit_text_areas().filter(_.getBuffer == buffer) 

164 

165 
def buffer_lock[A](buffer: JEditBuffer)(body: => A): A = 

166 
{ 

167 
try { buffer.readLock(); body } 

168 
finally { buffer.readUnlock() } 

169 
} 

49407  170 

50195
863b1dfc396c
prefer buffer_edit combinator over Javastyle boilerplate;
wenzelm
parents:
50186
diff
changeset

171 
def buffer_edit[A](buffer: JEditBuffer)(body: => A): A = 
863b1dfc396c
prefer buffer_edit combinator over Javastyle boilerplate;
wenzelm
parents:
50186
diff
changeset

172 
{ 
863b1dfc396c
prefer buffer_edit combinator over Javastyle boilerplate;
wenzelm
parents:
50186
diff
changeset

173 
try { buffer.beginCompoundEdit(); body } 
863b1dfc396c
prefer buffer_edit combinator over Javastyle boilerplate;
wenzelm
parents:
50186
diff
changeset

174 
finally { buffer.endCompoundEdit() } 
863b1dfc396c
prefer buffer_edit combinator over Javastyle boilerplate;
wenzelm
parents:
50186
diff
changeset

175 
} 
863b1dfc396c
prefer buffer_edit combinator over Javastyle boilerplate;
wenzelm
parents:
50186
diff
changeset

176 

49407  177 

50215  178 
/* get text */ 
179 

180 
def try_get_text(buffer: JEditBuffer, range: Text.Range): Option[String] = 

181 
try { Some(buffer.getText(range.start, range.length)) } 

182 
catch { case _: ArrayIndexOutOfBoundsException => None } 

183 

184 

50363
2f8dc9e65401
tuned signature in accordance to document operations;
wenzelm
parents:
50215
diff
changeset

185 
/* buffer range */ 
2f8dc9e65401
tuned signature in accordance to document operations;
wenzelm
parents:
50215
diff
changeset

186 

2f8dc9e65401
tuned signature in accordance to document operations;
wenzelm
parents:
50215
diff
changeset

187 
def buffer_range(buffer: JEditBuffer): Text.Range = 
2f8dc9e65401
tuned signature in accordance to document operations;
wenzelm
parents:
50215
diff
changeset

188 
Text.Range(0, (buffer.getLength  1) max 0) 
2f8dc9e65401
tuned signature in accordance to document operations;
wenzelm
parents:
50215
diff
changeset

189 

2f8dc9e65401
tuned signature in accordance to document operations;
wenzelm
parents:
50215
diff
changeset

190 

49407  191 
/* point range */ 
192 

193 
def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range = 

194 
buffer_lock(buffer) { 

195 
def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0) 

196 
try { 

197 
val c = text(offset) 

198 
if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1))) 

199 
Text.Range(offset, offset + 2) 

200 
else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset  1))) 

201 
Text.Range(offset  1, offset + 1) 

202 
else Text.Range(offset, offset + 1) 

203 
} 

204 
catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) } 

205 
} 

49408  206 

207 

208 
/* visible text range */ 

209 

210 
def visible_range(text_area: TextArea): Option[Text.Range] = 

211 
{ 

212 
val buffer = text_area.getBuffer 

213 
val n = text_area.getVisibleLines 

214 
if (n > 0) { 

215 
val start = text_area.getScreenLineStartOffset(0) 

216 
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

217 
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

218 
Some(Text.Range(start, end)) 
49408  219 
} 
220 
else None 

221 
} 

222 

223 
def invalidate_range(text_area: TextArea, range: Text.Range) 

224 
{ 

225 
val buffer = text_area.getBuffer 

226 
text_area.invalidateLineRange( 

227 
buffer.getLineOfOffset(range.start), 

228 
buffer.getLineOfOffset(range.stop)) 

229 
} 

49409  230 

231 

232 
/* graphics range */ 

233 

50115  234 
case class Gfx_Range(val x: Int, val y: Int, val length: Int) 
49409  235 

49843
afddf4e26fac
further refinement of jEdit line range, avoiding lack of final \n;
wenzelm
parents:
49712
diff
changeset

236 
// NB: jEdit always normalizes \r\n and \r to \n 
49409  237 
// NB: last line lacks \n 
238 
def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] = 

239 
{ 

51507  240 
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

241 
val char_width = (metric.unit * metric.average).round.toInt 
50849  242 

49409  243 
val buffer = text_area.getBuffer 
244 

245 
val end = buffer.getLength 

246 
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

247 

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

248 
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

249 
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

250 
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

251 
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

252 
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

253 
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

254 
(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

255 
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

256 
(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

257 
} 
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

258 
catch { case _: ArrayIndexOutOfBoundsException => (null, null, 0) } 
49409  259 

260 
if (p != null && q != null && p.x < q.x + r && p.y == q.y) 

50115  261 
Some(Gfx_Range(p.x, p.y, q.x + r  p.x)) 
49409  262 
else None 
263 
} 

49941
f2db0596bd61
more precise pixel_range: avoid popup when pointing into empty space after actual endofline;
wenzelm
parents:
49843
diff
changeset

264 

f2db0596bd61
more precise pixel_range: avoid popup when pointing into empty space after actual endofline;
wenzelm
parents:
49843
diff
changeset

265 

f2db0596bd61
more precise pixel_range: avoid popup when pointing into empty space after actual endofline;
wenzelm
parents:
49843
diff
changeset

266 
/* pixel range */ 
f2db0596bd61
more precise pixel_range: avoid popup when pointing into empty space after actual endofline;
wenzelm
parents:
49843
diff
changeset

267 

f2db0596bd61
more precise pixel_range: avoid popup when pointing into empty space after actual endofline;
wenzelm
parents:
49843
diff
changeset

268 
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 endofline;
wenzelm
parents:
49843
diff
changeset

269 
{ 
53183
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset

270 
// coordinates wrt. inner painter component 
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset

271 
val painter = text_area.getPainter 
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset

272 
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

273 
val offset = text_area.xyToOffset(x, y, false) 
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset

274 
if (offset >= 0) { 
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset

275 
val range = point_range(text_area.getBuffer, offset) 
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset

276 
gfx_range(text_area, range) match { 
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset

277 
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

278 
case _ => None 
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset

279 
} 
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset

280 
} 
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset

281 
else None 
49941
f2db0596bd61
more precise pixel_range: avoid popup when pointing into empty space after actual endofline;
wenzelm
parents:
49843
diff
changeset

282 
} 
53183
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset

283 
else None 
49941
f2db0596bd61
more precise pixel_range: avoid popup when pointing into empty space after actual endofline;
wenzelm
parents:
49843
diff
changeset

284 
} 
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

285 

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

286 

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

287 
/* 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

288 

51507  289 
abstract class Pretty_Metric extends Pretty.Metric 
290 
{ 

291 
def average: Double 

292 
} 

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

293 

51507  294 
def pretty_metric(painter: TextAreaPainter): Pretty_Metric = 
295 
new Pretty_Metric { 

296 
def string_width(s: String): Double = 

297 
painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth 

298 

299 
val unit = string_width(Pretty.space) 

300 
val average = string_width("mix") / (3 * unit) 

301 
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

302 
} 
52873  303 

304 

305 
/* icons */ 

306 

307 
def load_icon(name: String): Icon = 

308 
{ 

309 
val name1 = 

310 
if (name.startsWith("ideaicons/")) { 

311 
val file = 

312 
Isabelle_System.platform_file_url(Path.explode("$JEDIT_HOME/dist/jars/ideaicons.jar")) 

313 
"jar:" + file + "!/" + name 

314 
} 

315 
else name 

316 
val icon = GUIUtilities.loadIcon(name1) 

317 
if (icon.getIconWidth < 0  icon.getIconHeight < 0) error("Bad icon: " + name) 

318 
else icon 

319 
} 

52874  320 

321 
def load_image_icon(name: String): ImageIcon = 

322 
load_icon(name) match { 

323 
case icon: ImageIcon => icon 

324 
case _ => error("Bad image icon: " + name) 

325 
} 

53226
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset

326 

9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset

327 

53231
423e29f1f304
avoid complication and event duplication due to KeyEventInterceptor  NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents:
53226
diff
changeset

328 
/* key event handling */ 
423e29f1f304
avoid complication and event duplication due to KeyEventInterceptor  NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents:
53226
diff
changeset

329 

423e29f1f304
avoid complication and event duplication due to KeyEventInterceptor  NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents:
53226
diff
changeset

330 
def request_focus_view 
423e29f1f304
avoid complication and event duplication due to KeyEventInterceptor  NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents:
53226
diff
changeset

331 
{ 
423e29f1f304
avoid complication and event duplication due to KeyEventInterceptor  NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents:
53226
diff
changeset

332 
val view = jEdit.getActiveView() 
423e29f1f304
avoid complication and event duplication due to KeyEventInterceptor  NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents:
53226
diff
changeset

333 
if (view != null) { 
423e29f1f304
avoid complication and event duplication due to KeyEventInterceptor  NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents:
53226
diff
changeset

334 
val text_area = view.getTextArea 
423e29f1f304
avoid complication and event duplication due to KeyEventInterceptor  NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents:
53226
diff
changeset

335 
if (text_area != null) text_area.requestFocus 
423e29f1f304
avoid complication and event duplication due to KeyEventInterceptor  NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents:
53226
diff
changeset

336 
} 
423e29f1f304
avoid complication and event duplication due to KeyEventInterceptor  NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents:
53226
diff
changeset

337 
} 
423e29f1f304
avoid complication and event duplication due to KeyEventInterceptor  NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents:
53226
diff
changeset

338 

423e29f1f304
avoid complication and event duplication due to KeyEventInterceptor  NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents:
53226
diff
changeset

339 
def propagate_key(view: View, evt: KeyEvent) 
423e29f1f304
avoid complication and event duplication due to KeyEventInterceptor  NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents:
53226
diff
changeset

340 
{ 
423e29f1f304
avoid complication and event duplication due to KeyEventInterceptor  NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents:
53226
diff
changeset

341 
if (view != null && !evt.isConsumed) 
423e29f1f304
avoid complication and event duplication due to KeyEventInterceptor  NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents:
53226
diff
changeset

342 
view.getInputHandler().processKeyEvent(evt, View.ACTION_BAR, false) 
423e29f1f304
avoid complication and event duplication due to KeyEventInterceptor  NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents:
53226
diff
changeset

343 
} 
53226
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset

344 

9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset

345 
def key_listener( 
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset

346 
key_typed: KeyEvent => Unit = _ => (), 
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset

347 
key_pressed: KeyEvent => Unit = _ => (), 
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset

348 
key_released: KeyEvent => Unit = _ => ()): KeyListener = 
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset

349 
{ 
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset

350 
def process_key_event(evt0: KeyEvent, handle: KeyEvent => Unit) 
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset

351 
{ 
53237  352 
val evt = KeyEventWorkaround.processKeyEvent(evt0) 
53226
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset

353 
if (evt != null) handle(evt) 
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset

354 
} 
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset

355 

9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset

356 
new KeyListener 
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset

357 
{ 
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset

358 
def keyTyped(evt: KeyEvent) { process_key_event(evt, key_typed) } 
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset

359 
def keyPressed(evt: KeyEvent) { process_key_event(evt, key_pressed) } 
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset

360 
def keyReleased(evt: KeyEvent) { process_key_event(evt, key_released) } 
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset

361 
} 
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset

362 
} 
49406  363 
} 
364 