author | wenzelm |
Fri, 22 May 2020 11:30:06 +0200 | |
changeset 71861 | 1330fa4a2b85 |
parent 71601 | 97ccf48c2f0c |
child 72899 | 8732315dfafa |
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 |
||
65469 | 12 |
import java.io.{File => JFile} |
53712 | 13 |
import java.awt.{Component, Container, GraphicsEnvironment, Point, Rectangle, Dimension} |
53784 | 14 |
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
|
15 |
import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities} |
49710
21d88a631fcc
refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents:
49409
diff
changeset
|
16 |
|
56823
37be55461dbe
more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents:
56774
diff
changeset
|
17 |
import scala.util.parsing.input.CharSequenceReader |
49406 | 18 |
|
62264
340f98836fd9
re-init document views for the sake of Text_Overview size;
wenzelm
parents:
61865
diff
changeset
|
19 |
import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug, EditPane} |
65469 | 20 |
import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager} |
53226
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset
|
21 |
import org.gjt.sp.jedit.gui.KeyEventWorkaround |
61192 | 22 |
import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager} |
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
|
23 |
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter} |
49406 | 24 |
|
25 |
||
26 |
object JEdit_Lib |
|
27 |
{ |
|
71861 | 28 |
/* jEdit directories */ |
29 |
||
30 |
def directories: List[JFile] = |
|
31 |
(Option(jEdit.getSettingsDirectory).toList ::: List(jEdit.getJEditHome)).map(new JFile(_)) |
|
32 |
||
33 |
||
53247
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset
|
34 |
/* location within multi-screen environment */ |
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset
|
35 |
|
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset
|
36 |
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
|
37 |
{ |
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset
|
38 |
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
|
39 |
{ |
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset
|
40 |
val w = size.width |
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset
|
41 |
val h = size.height |
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
|
42 |
|
53247
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset
|
43 |
val x0 = parent.getLocationOnScreen.x |
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset
|
44 |
val y0 = parent.getLocationOnScreen.y |
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset
|
45 |
val x1 = x0 + parent.getWidth - w |
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset
|
46 |
val y1 = y0 + parent.getHeight - h |
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset
|
47 |
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
|
48 |
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
|
49 |
|
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset
|
50 |
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
|
51 |
SwingUtilities.convertPointFromScreen(location, parent) |
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset
|
52 |
location |
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset
|
53 |
} |
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset
|
54 |
} |
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset
|
55 |
|
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset
|
56 |
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 multi-screen environment;
wenzelm
parents:
50363
diff
changeset
|
57 |
{ |
53247
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset
|
58 |
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
|
59 |
SwingUtilities.convertPointToScreen(screen_point, component) |
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset
|
60 |
|
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
|
61 |
val ge = GraphicsEnvironment.getLocalGraphicsEnvironment |
53247
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset
|
62 |
val screen_bounds = |
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset
|
63 |
(for { |
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset
|
64 |
device <- ge.getScreenDevices.iterator |
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset
|
65 |
config <- device.getConfigurations.iterator |
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset
|
66 |
bounds = config.getBounds |
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset
|
67 |
} 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
|
68 |
|
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53237
diff
changeset
|
69 |
Screen_Location(screen_point, screen_bounds) |
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
|
70 |
} |
0493efcc97e9
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents:
50363
diff
changeset
|
71 |
|
0493efcc97e9
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents:
50363
diff
changeset
|
72 |
|
53019 | 73 |
/* window geometry measurement */ |
74 |
||
75 |
private lazy val dummy_window = new JWindow |
|
76 |
||
77 |
final case class Window_Geometry(width: Int, height: Int, inner_width: Int, inner_height: Int) |
|
78 |
{ |
|
79 |
def deco_width: Int = width - inner_width |
|
80 |
def deco_height: Int = height - inner_height |
|
81 |
} |
|
82 |
||
83 |
def window_geometry(outer: Container, inner: Component): Window_Geometry = |
|
84 |
{ |
|
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56930
diff
changeset
|
85 |
GUI_Thread.require {} |
53019 | 86 |
|
87 |
val old_content = dummy_window.getContentPane |
|
88 |
||
89 |
dummy_window.setContentPane(outer) |
|
90 |
dummy_window.pack |
|
91 |
dummy_window.revalidate |
|
92 |
||
93 |
val geometry = |
|
94 |
Window_Geometry( |
|
95 |
dummy_window.getWidth, dummy_window.getHeight, inner.getWidth, inner.getHeight) |
|
96 |
||
97 |
dummy_window.setContentPane(old_content) |
|
98 |
||
99 |
geometry |
|
100 |
} |
|
101 |
||
102 |
||
65469 | 103 |
/* files */ |
104 |
||
105 |
def is_file(name: String): Boolean = |
|
106 |
VFSManager.getVFSForPath(name).isInstanceOf[FileVFS] |
|
107 |
||
108 |
def check_file(name: String): Option[JFile] = |
|
109 |
if (is_file(name)) Some(new JFile(name)) else None |
|
110 |
||
111 |
||
49406 | 112 |
/* buffers */ |
113 |
||
114 |
def buffer_text(buffer: JEditBuffer): String = |
|
115 |
buffer_lock(buffer) { buffer.getText(0, buffer.getLength) } |
|
116 |
||
56823
37be55461dbe
more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents:
56774
diff
changeset
|
117 |
def buffer_reader(buffer: JEditBuffer): CharSequenceReader = |
64824 | 118 |
Scan.char_reader(buffer.getSegment(0, buffer.getLength)) |
56823
37be55461dbe
more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents:
56774
diff
changeset
|
119 |
|
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53247
diff
changeset
|
120 |
def buffer_mode(buffer: JEditBuffer): String = |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53247
diff
changeset
|
121 |
{ |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53247
diff
changeset
|
122 |
val mode = buffer.getMode |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53247
diff
changeset
|
123 |
if (mode == null) "" |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53247
diff
changeset
|
124 |
else { |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53247
diff
changeset
|
125 |
val name = mode.getName |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53247
diff
changeset
|
126 |
if (name == null) "" else name |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53247
diff
changeset
|
127 |
} |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53247
diff
changeset
|
128 |
} |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53247
diff
changeset
|
129 |
|
65469 | 130 |
def buffer_line_manager(buffer: JEditBuffer): LineManager = |
131 |
Untyped.get[LineManager](buffer, "lineMgr") |
|
132 |
||
49406 | 133 |
def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath |
134 |
||
65469 | 135 |
def buffer_file(buffer: Buffer): Option[JFile] = check_file(buffer_name(buffer)) |
61192 | 136 |
|
68060
3931ed905e93
avoid output showing up in kill ring (via TextArea.setText, JEditBuffer.remove, UndoManager.contentRemoved), e.g. relevant for action "paste-deleted";
wenzelm
parents:
67014
diff
changeset
|
137 |
def buffer_undo_in_progress[A](buffer: JEditBuffer, body: => A): A = |
3931ed905e93
avoid output showing up in kill ring (via TextArea.setText, JEditBuffer.remove, UndoManager.contentRemoved), e.g. relevant for action "paste-deleted";
wenzelm
parents:
67014
diff
changeset
|
138 |
{ |
3931ed905e93
avoid output showing up in kill ring (via TextArea.setText, JEditBuffer.remove, UndoManager.contentRemoved), e.g. relevant for action "paste-deleted";
wenzelm
parents:
67014
diff
changeset
|
139 |
val undo_in_progress = buffer.isUndoInProgress |
3931ed905e93
avoid output showing up in kill ring (via TextArea.setText, JEditBuffer.remove, UndoManager.contentRemoved), e.g. relevant for action "paste-deleted";
wenzelm
parents:
67014
diff
changeset
|
140 |
def set(b: Boolean) { Untyped.set[Boolean](buffer, "undoInProgress", b) } |
3931ed905e93
avoid output showing up in kill ring (via TextArea.setText, JEditBuffer.remove, UndoManager.contentRemoved), e.g. relevant for action "paste-deleted";
wenzelm
parents:
67014
diff
changeset
|
141 |
try { set(true); body } finally { set(undo_in_progress) } |
3931ed905e93
avoid output showing up in kill ring (via TextArea.setText, JEditBuffer.remove, UndoManager.contentRemoved), e.g. relevant for action "paste-deleted";
wenzelm
parents:
67014
diff
changeset
|
142 |
} |
3931ed905e93
avoid output showing up in kill ring (via TextArea.setText, JEditBuffer.remove, UndoManager.contentRemoved), e.g. relevant for action "paste-deleted";
wenzelm
parents:
67014
diff
changeset
|
143 |
|
49406 | 144 |
|
145 |
/* main jEdit components */ |
|
146 |
||
147 |
def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator |
|
148 |
||
149 |
def jedit_buffer(name: String): Option[Buffer] = |
|
150 |
jedit_buffers().find(buffer => buffer_name(buffer) == name) |
|
151 |
||
56457
eea4bbe15745
tuned signature -- prefer static type Document.Node.Name;
wenzelm
parents:
55812
diff
changeset
|
152 |
def jedit_buffer(name: Document.Node.Name): Option[Buffer] = |
eea4bbe15745
tuned signature -- prefer static type Document.Node.Name;
wenzelm
parents:
55812
diff
changeset
|
153 |
jedit_buffer(name.node) |
eea4bbe15745
tuned signature -- prefer static type Document.Node.Name;
wenzelm
parents:
55812
diff
changeset
|
154 |
|
49406 | 155 |
def jedit_views(): Iterator[View] = jEdit.getViews().iterator |
156 |
||
69636 | 157 |
def jedit_view(view: View = null): View = |
158 |
if (view == null) jEdit.getActiveView() else view |
|
159 |
||
62264
340f98836fd9
re-init document views for the sake of Text_Overview size;
wenzelm
parents:
61865
diff
changeset
|
160 |
def jedit_edit_panes(view: View): Iterator[EditPane] = |
340f98836fd9
re-init document views for the sake of Text_Overview size;
wenzelm
parents:
61865
diff
changeset
|
161 |
if (view == null) Iterator.empty |
340f98836fd9
re-init document views for the sake of Text_Overview size;
wenzelm
parents:
61865
diff
changeset
|
162 |
else view.getEditPanes().iterator.filter(_ != null) |
340f98836fd9
re-init document views for the sake of Text_Overview size;
wenzelm
parents:
61865
diff
changeset
|
163 |
|
49406 | 164 |
def jedit_text_areas(view: View): Iterator[JEditTextArea] = |
56587
83777a91f5de
clarified before_caret_range: prevent continuation on next line;
wenzelm
parents:
56574
diff
changeset
|
165 |
if (view == null) Iterator.empty |
83777a91f5de
clarified before_caret_range: prevent continuation on next line;
wenzelm
parents:
56574
diff
changeset
|
166 |
else view.getEditPanes().iterator.filter(_ != null).map(_.getTextArea).filter(_ != null) |
49406 | 167 |
|
168 |
def jedit_text_areas(): Iterator[JEditTextArea] = |
|
71601 | 169 |
jedit_views().flatMap(jedit_text_areas) |
49406 | 170 |
|
171 |
def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] = |
|
172 |
jedit_text_areas().filter(_.getBuffer == buffer) |
|
173 |
||
174 |
def buffer_lock[A](buffer: JEditBuffer)(body: => A): A = |
|
175 |
{ |
|
176 |
try { buffer.readLock(); body } |
|
177 |
finally { buffer.readUnlock() } |
|
178 |
} |
|
49407 | 179 |
|
50195
863b1dfc396c
prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents:
50186
diff
changeset
|
180 |
def buffer_edit[A](buffer: JEditBuffer)(body: => A): A = |
863b1dfc396c
prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents:
50186
diff
changeset
|
181 |
{ |
863b1dfc396c
prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents:
50186
diff
changeset
|
182 |
try { buffer.beginCompoundEdit(); body } |
863b1dfc396c
prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents:
50186
diff
changeset
|
183 |
finally { buffer.endCompoundEdit() } |
863b1dfc396c
prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents:
50186
diff
changeset
|
184 |
} |
863b1dfc396c
prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents:
50186
diff
changeset
|
185 |
|
49407 | 186 |
|
50215 | 187 |
/* get text */ |
188 |
||
67014 | 189 |
def get_text(buffer: JEditBuffer, range: Text.Range): Option[String] = |
50215 | 190 |
try { Some(buffer.getText(range.start, range.length)) } |
191 |
catch { case _: ArrayIndexOutOfBoundsException => None } |
|
192 |
||
193 |
||
49407 | 194 |
/* point range */ |
195 |
||
196 |
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
|
197 |
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
|
198 |
else |
5157f7615e99
prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents:
56589
diff
changeset
|
199 |
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
|
200 |
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
|
201 |
try { |
5157f7615e99
prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents:
56589
diff
changeset
|
202 |
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
|
203 |
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
|
204 |
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
|
205 |
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
|
206 |
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
|
207 |
else |
5157f7615e99
prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents:
56589
diff
changeset
|
208 |
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
|
209 |
} |
5157f7615e99
prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents:
56589
diff
changeset
|
210 |
catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) } |
49407 | 211 |
} |
49408 | 212 |
|
213 |
||
55812 | 214 |
/* text ranges */ |
215 |
||
216 |
def buffer_range(buffer: JEditBuffer): Text.Range = |
|
217 |
Text.Range(0, buffer.getLength) |
|
49408 | 218 |
|
56587
83777a91f5de
clarified before_caret_range: prevent continuation on next line;
wenzelm
parents:
56574
diff
changeset
|
219 |
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
|
220 |
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
|
221 |
|
56592
5157f7615e99
prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents:
56589
diff
changeset
|
222 |
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
|
223 |
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
|
224 |
|
49408 | 225 |
def visible_range(text_area: TextArea): Option[Text.Range] = |
226 |
{ |
|
227 |
val buffer = text_area.getBuffer |
|
228 |
val n = text_area.getVisibleLines |
|
229 |
if (n > 0) { |
|
230 |
val start = text_area.getScreenLineStartOffset(0) |
|
231 |
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
|
232 |
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
|
233 |
Some(Text.Range(start, end)) |
49408 | 234 |
} |
235 |
else None |
|
236 |
} |
|
237 |
||
238 |
def invalidate_range(text_area: TextArea, range: Text.Range) |
|
239 |
{ |
|
240 |
val buffer = text_area.getBuffer |
|
55812 | 241 |
buffer_range(buffer).try_restrict(range) match { |
242 |
case Some(range1) if !range1.is_singularity => |
|
56699 | 243 |
try { |
244 |
text_area.invalidateLineRange( |
|
245 |
buffer.getLineOfOffset(range1.start), |
|
246 |
buffer.getLineOfOffset(range1.stop)) |
|
247 |
} |
|
248 |
catch { case _: ArrayIndexOutOfBoundsException => } |
|
55812 | 249 |
case _ => |
250 |
} |
|
49408 | 251 |
} |
49409 | 252 |
|
62986 | 253 |
def invalidate(text_area: TextArea) |
254 |
{ |
|
255 |
val visible_lines = text_area.getVisibleLines |
|
256 |
if (visible_lines > 0) text_area.invalidateScreenLineRange(0, visible_lines) |
|
257 |
} |
|
258 |
||
49409 | 259 |
|
260 |
/* graphics range */ |
|
261 |
||
60215 | 262 |
case class Gfx_Range(x: Int, y: Int, length: Int) |
49409 | 263 |
|
49843
afddf4e26fac
further refinement of jEdit line range, avoiding lack of final \n;
wenzelm
parents:
49712
diff
changeset
|
264 |
// NB: jEdit always normalizes \r\n and \r to \n |
49409 | 265 |
// NB: last line lacks \n |
266 |
def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] = |
|
267 |
{ |
|
51507 | 268 |
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
|
269 |
val char_width = (metric.unit * metric.average).round.toInt |
50849 | 270 |
|
49409 | 271 |
val buffer = text_area.getBuffer |
272 |
||
273 |
val end = buffer.getLength |
|
274 |
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
|
275 |
|
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
|
276 |
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
|
277 |
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
|
278 |
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
|
279 |
val (q, r) = |
67014 | 280 |
if (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
|
281 |
(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 second-last line;
wenzelm
parents:
53786
diff
changeset
|
282 |
else if (stop >= end) |
5c40782f68b3
clarified special eol treatment (amending 3d55ef732cd7): allow last line to be empty, which means stop == end for second-last line;
wenzelm
parents:
53786
diff
changeset
|
283 |
(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
|
284 |
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
|
285 |
(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
|
286 |
} |
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
|
287 |
catch { case _: ArrayIndexOutOfBoundsException => (null, null, 0) } |
49409 | 288 |
|
289 |
if (p != null && q != null && p.x < q.x + r && p.y == q.y) |
|
50115 | 290 |
Some(Gfx_Range(p.x, p.y, q.x + r - p.x)) |
49409 | 291 |
else None |
292 |
} |
|
49941
f2db0596bd61
more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents:
49843
diff
changeset
|
293 |
|
f2db0596bd61
more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents:
49843
diff
changeset
|
294 |
|
f2db0596bd61
more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents:
49843
diff
changeset
|
295 |
/* pixel range */ |
f2db0596bd61
more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents:
49843
diff
changeset
|
296 |
|
f2db0596bd61
more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents:
49843
diff
changeset
|
297 |
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
|
298 |
{ |
53183
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset
|
299 |
// coordinates wrt. inner painter component |
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset
|
300 |
val painter = text_area.getPainter |
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset
|
301 |
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
|
302 |
val offset = text_area.xyToOffset(x, y, false) |
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset
|
303 |
if (offset >= 0) { |
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset
|
304 |
val range = point_range(text_area.getBuffer, offset) |
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset
|
305 |
gfx_range(text_area, range) match { |
60215 | 306 |
case Some(g) if g.x <= x && x < g.x + g.length => Some(range) |
53183
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset
|
307 |
case _ => None |
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset
|
308 |
} |
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset
|
309 |
} |
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset
|
310 |
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
|
311 |
} |
53183
018d71bee930
strict checking of coordinates wrt. inner painter component;
wenzelm
parents:
53019
diff
changeset
|
312 |
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
|
313 |
} |
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
|
314 |
|
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
|
315 |
|
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
|
316 |
/* 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
|
317 |
|
51507 | 318 |
abstract class Pretty_Metric extends Pretty.Metric |
319 |
{ |
|
320 |
def average: Double |
|
321 |
} |
|
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
|
322 |
|
51507 | 323 |
def pretty_metric(painter: TextAreaPainter): Pretty_Metric = |
324 |
new Pretty_Metric { |
|
325 |
def string_width(s: String): Double = |
|
326 |
painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth |
|
327 |
||
71601 | 328 |
val unit: Double = string_width(Symbol.space) max 1.0 |
329 |
val average: Double = string_width("mix") / (3 * unit) |
|
51507 | 330 |
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
|
331 |
} |
52873 | 332 |
|
333 |
||
334 |
/* icons */ |
|
335 |
||
336 |
def load_icon(name: String): Icon = |
|
337 |
{ |
|
338 |
val name1 = |
|
339 |
if (name.startsWith("idea-icons/")) { |
|
64770 | 340 |
val file = Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar").file.toURI.toASCIIString |
52873 | 341 |
"jar:" + file + "!/" + name |
342 |
} |
|
343 |
else name |
|
344 |
val icon = GUIUtilities.loadIcon(name1) |
|
345 |
if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name) |
|
346 |
else icon |
|
347 |
} |
|
52874 | 348 |
|
349 |
def load_image_icon(name: String): ImageIcon = |
|
350 |
load_icon(name) match { |
|
351 |
case icon: ImageIcon => icon |
|
352 |
case _ => error("Bad image icon: " + name) |
|
353 |
} |
|
53226
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 |
|
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
|
356 |
/* 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
|
357 |
|
66592 | 358 |
def request_focus_view(alt_view: View = null) |
359 |
{ |
|
360 |
isabelle.jedit_base.JEdit_Lib.request_focus_view(alt_view) |
|
361 |
} |
|
362 |
||
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
|
363 |
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
|
364 |
{ |
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
|
365 |
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
|
366 |
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
|
367 |
} |
53226
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset
|
368 |
|
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset
|
369 |
def key_listener( |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset
|
370 |
key_typed: KeyEvent => Unit = _ => (), |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset
|
371 |
key_pressed: KeyEvent => Unit = _ => (), |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset
|
372 |
key_released: KeyEvent => Unit = _ => ()): KeyListener = |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset
|
373 |
{ |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset
|
374 |
def process_key_event(evt0: KeyEvent, handle: KeyEvent => Unit) |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset
|
375 |
{ |
53237 | 376 |
val evt = KeyEventWorkaround.processKeyEvent(evt0) |
53226
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset
|
377 |
if (evt != null) handle(evt) |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset
|
378 |
} |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset
|
379 |
|
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset
|
380 |
new KeyListener |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset
|
381 |
{ |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset
|
382 |
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
|
383 |
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
|
384 |
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
|
385 |
} |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53183
diff
changeset
|
386 |
} |
53784 | 387 |
|
388 |
def special_key(evt: KeyEvent): Boolean = |
|
389 |
{ |
|
59571 | 390 |
// cf. 5.2.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java |
71500 | 391 |
val mod = evt.getModifiersEx |
392 |
(mod & InputEvent.CTRL_DOWN_MASK) != 0 && (mod & InputEvent.ALT_DOWN_MASK) == 0 || |
|
393 |
(mod & InputEvent.CTRL_DOWN_MASK) == 0 && (mod & InputEvent.ALT_DOWN_MASK) != 0 && |
|
53784 | 394 |
!Debug.ALT_KEY_PRESSED_DISABLED || |
71500 | 395 |
(mod & InputEvent.META_DOWN_MASK) != 0 |
53784 | 396 |
} |
49406 | 397 |
} |