author  wenzelm 
Tue, 15 Apr 2014 19:27:50 +0200  
changeset 56592  5157f7615e99 
parent 56589  71c5d1f516c0 
child 56593  0ea7c84110ac 
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 

53712  12 
import java.awt.{Component, Container, GraphicsEnvironment, Point, Rectangle, Dimension} 
53784  13 
import java.awt.event.{InputEvent, 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 

53784  18 
import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug} 
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 

49406  95 
/* buffers */ 
96 

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

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

99 

100 
def buffer_text(buffer: JEditBuffer): String = 

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

102 

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

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

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

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

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

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

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

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

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

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

112 

49406  113 
def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath 
114 

115 

116 
/* main jEdit components */ 

117 

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

119 

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

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

122 

56457
eea4bbe15745
tuned signature  prefer static type Document.Node.Name;
wenzelm
parents:
55812
diff
changeset

123 
def jedit_buffer(name: Document.Node.Name): Option[Buffer] = 
eea4bbe15745
tuned signature  prefer static type Document.Node.Name;
wenzelm
parents:
55812
diff
changeset

124 
jedit_buffer(name.node) 
eea4bbe15745
tuned signature  prefer static type Document.Node.Name;
wenzelm
parents:
55812
diff
changeset

125 

49406  126 
def jedit_views(): Iterator[View] = jEdit.getViews().iterator 
127 

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

56587
83777a91f5de
clarified before_caret_range: prevent continuation on next line;
wenzelm
parents:
56574
diff
changeset

129 
if (view == null) Iterator.empty 
83777a91f5de
clarified before_caret_range: prevent continuation on next line;
wenzelm
parents:
56574
diff
changeset

130 
else view.getEditPanes().iterator.filter(_ != null).map(_.getTextArea).filter(_ != null) 
49406  131 

132 
def jedit_text_areas(): Iterator[JEditTextArea] = 

133 
jedit_views().flatMap(jedit_text_areas(_)) 

134 

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

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

137 

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

139 
{ 

140 
try { buffer.readLock(); body } 

141 
finally { buffer.readUnlock() } 

142 
} 

49407  143 

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

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

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

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

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

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

149 

49407  150 

50215  151 
/* get text */ 
152 

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

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

155 
catch { case _: ArrayIndexOutOfBoundsException => None } 

156 

53784  157 
def try_get_text(text: String, range: Text.Range): Option[String] = 
158 
try { Some(text.substring(range.start, range.stop)) } 

159 
catch { case _: IndexOutOfBoundsException => None } 

160 

50215  161 

49407  162 
/* point range */ 
163 

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

56592
5157f7615e99
prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents:
56589
diff
changeset

165 
if (offset < 0) Text.Range.offside 
5157f7615e99
prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents:
56589
diff
changeset

166 
else 
5157f7615e99
prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents:
56589
diff
changeset

167 
buffer_lock(buffer) { 
5157f7615e99
prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents:
56589
diff
changeset

168 
def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0) 
5157f7615e99
prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents:
56589
diff
changeset

169 
try { 
5157f7615e99
prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents:
56589
diff
changeset

170 
val c = text(offset) 
5157f7615e99
prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents:
56589
diff
changeset

171 
if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1))) 
5157f7615e99
prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents:
56589
diff
changeset

172 
Text.Range(offset, offset + 2) 
5157f7615e99
prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents:
56589
diff
changeset

173 
else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset  1))) 
5157f7615e99
prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents:
56589
diff
changeset

174 
Text.Range(offset  1, offset + 1) 
5157f7615e99
prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents:
56589
diff
changeset

175 
else 
5157f7615e99
prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents:
56589
diff
changeset

176 
Text.Range(offset, offset + 1) 
5157f7615e99
prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents:
56589
diff
changeset

177 
} 
5157f7615e99
prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents:
56589
diff
changeset

178 
catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) } 
49407  179 
} 
49408  180 

181 

55812  182 
/* text ranges */ 
183 

184 
def buffer_range(buffer: JEditBuffer): Text.Range = 

185 
Text.Range(0, buffer.getLength) 

49408  186 

56587
83777a91f5de
clarified before_caret_range: prevent continuation on next line;
wenzelm
parents:
56574
diff
changeset

187 
def line_range(buffer: JEditBuffer, line: Int): Text.Range = 
56589
71c5d1f516c0
more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line;
wenzelm
parents:
56587
diff
changeset

188 
Text.Range(buffer.getLineStartOffset(line), buffer.getLineEndOffset(line) min buffer.getLength) 
56587
83777a91f5de
clarified before_caret_range: prevent continuation on next line;
wenzelm
parents:
56574
diff
changeset

189 

56592
5157f7615e99
prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents:
56589
diff
changeset

190 
def caret_range(text_area: TextArea): Text.Range = 
5157f7615e99
prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents:
56589
diff
changeset

191 
point_range(text_area.getBuffer, text_area.getCaretPosition) 
5157f7615e99
prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents:
56589
diff
changeset

192 

56587
83777a91f5de
clarified before_caret_range: prevent continuation on next line;
wenzelm
parents:
56574
diff
changeset

193 
def before_caret_range(text_area: TextArea, rendering: Rendering): Option[Text.Range] = 
83777a91f5de
clarified before_caret_range: prevent continuation on next line;
wenzelm
parents:
56574
diff
changeset

194 
{ 
83777a91f5de
clarified before_caret_range: prevent continuation on next line;
wenzelm
parents:
56574
diff
changeset

195 
val range = line_range(text_area.getBuffer, text_area.getCaretLine) 
83777a91f5de
clarified before_caret_range: prevent continuation on next line;
wenzelm
parents:
56574
diff
changeset

196 
val snapshot = rendering.snapshot 
83777a91f5de
clarified before_caret_range: prevent continuation on next line;
wenzelm
parents:
56574
diff
changeset

197 
val former_caret = snapshot.revert(text_area.getCaretPosition) 
83777a91f5de
clarified before_caret_range: prevent continuation on next line;
wenzelm
parents:
56574
diff
changeset

198 
snapshot.convert(Text.Range(former_caret  1, former_caret)).try_restrict(range) 
83777a91f5de
clarified before_caret_range: prevent continuation on next line;
wenzelm
parents:
56574
diff
changeset

199 
} 
83777a91f5de
clarified before_caret_range: prevent continuation on next line;
wenzelm
parents:
56574
diff
changeset

200 

49408  201 
def visible_range(text_area: TextArea): Option[Text.Range] = 
202 
{ 

203 
val buffer = text_area.getBuffer 

204 
val n = text_area.getVisibleLines 

205 
if (n > 0) { 

206 
val start = text_area.getScreenLineStartOffset(0) 

207 
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

208 
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

209 
Some(Text.Range(start, end)) 
49408  210 
} 
211 
else None 

212 
} 

213 

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

215 
{ 

216 
val buffer = text_area.getBuffer 

55812  217 
buffer_range(buffer).try_restrict(range) match { 
218 
case Some(range1) if !range1.is_singularity => 

219 
text_area.invalidateLineRange( 

220 
buffer.getLineOfOffset(range1.start), 

221 
buffer.getLineOfOffset(range1.stop)) 

222 
case _ => 

223 
} 

49408  224 
} 
49409  225 

226 

227 
/* graphics range */ 

228 

50115  229 
case class Gfx_Range(val x: Int, val y: Int, val length: Int) 
49409  230 

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

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

234 
{ 

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

236 
val char_width = (metric.unit * metric.average).round.toInt 
50849  237 

49409  238 
val buffer = text_area.getBuffer 
239 

240 
val end = buffer.getLength 

241 
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

242 

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

243 
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

244 
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

245 
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

246 
val (q, r) = 
55549
5c40782f68b3
clarified special eol treatment (amending 3d55ef732cd7): allow last line to be empty, which means stop == end for secondlast line;
wenzelm
parents:
53786
diff
changeset

247 
if (try_get_text(buffer, Text.Range(stop  1, stop)) == Some("\n")) 
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

248 
(text_area.offsetToXY(stop  1), char_width) 
55549
5c40782f68b3
clarified special eol treatment (amending 3d55ef732cd7): allow last line to be empty, which means stop == end for secondlast line;
wenzelm
parents:
53786
diff
changeset

249 
else if (stop >= end) 
5c40782f68b3
clarified special eol treatment (amending 3d55ef732cd7): allow last line to be empty, which means stop == end for secondlast line;
wenzelm
parents:
53786
diff
changeset

250 
(text_area.offsetToXY(end), char_width * (stop  end)) 
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

251 
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

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

253 
} 
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 
catch { case _: ArrayIndexOutOfBoundsException => (null, null, 0) } 
49409  255 

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

50115  257 
Some(Gfx_Range(p.x, p.y, q.x + r  p.x)) 
49409  258 
else None 
259 
} 

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

260 

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

261 

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

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

263 

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

264 
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

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

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

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

268 
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

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

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

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

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

273 
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

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

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

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

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

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

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

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

281 

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

282 

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

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

284 

51507  285 
abstract class Pretty_Metric extends Pretty.Metric 
286 
{ 

287 
def average: Double 

288 
} 

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

289 

51507  290 
def pretty_metric(painter: TextAreaPainter): Pretty_Metric = 
291 
new Pretty_Metric { 

292 
def string_width(s: String): Double = 

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

294 

295 
val unit = string_width(Pretty.space) 

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

297 
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

298 
} 
52873  299 

300 

301 
/* icons */ 

302 

303 
def load_icon(name: String): Icon = 

304 
{ 

305 
val name1 = 

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

307 
val file = 

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

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

310 
} 

311 
else name 

312 
val icon = GUIUtilities.loadIcon(name1) 

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

314 
else icon 

315 
} 

52874  316 

317 
def load_image_icon(name: String): ImageIcon = 

318 
load_icon(name) match { 

319 
case icon: ImageIcon => icon 

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

321 
} 

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

322 

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

323 

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

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

325 

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

326 
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

327 
{ 
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 
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

329 
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

330 
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

331 
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

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

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

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

338 
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

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

340 

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

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

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

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

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

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

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

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

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

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

351 

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

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

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

354 
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

355 
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

356 
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

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

358 
} 
53784  359 

360 
def special_key(evt: KeyEvent): Boolean = 

361 
{ 

362 
// cf. 5.1.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java 

363 
val mod = evt.getModifiers 

364 
(mod & InputEvent.CTRL_MASK) != 0 && (mod & InputEvent.ALT_MASK) == 0  

365 
(mod & InputEvent.CTRL_MASK) == 0 && (mod & InputEvent.ALT_MASK) != 0 && 

366 
!Debug.ALT_KEY_PRESSED_DISABLED  

367 
(mod & InputEvent.META_MASK) != 0 

368 
} 

49406  369 
} 
370 