--- a/src/Tools/jEdit/src/jedit_lib.scala Mon Apr 14 20:36:50 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala Mon Apr 14 21:51:41 2014 +0200
@@ -176,6 +176,16 @@
}
+ /* caret */
+
+ def before_caret_range(text_area: TextArea, rendering: Rendering): Text.Range =
+ {
+ val snapshot = rendering.snapshot
+ val former_caret = snapshot.revert(text_area.getCaretPosition)
+ snapshot.convert(Text.Range(former_caret - 1, former_caret))
+ }
+
+
/* text ranges */
def buffer_range(buffer: JEditBuffer): Text.Range =