--- a/src/Tools/jEdit/src/jedit_lib.scala Tue Dec 20 18:11:42 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Tue Dec 20 21:35:56 2016 +0100
@@ -198,7 +198,7 @@
def caret_range(text_area: TextArea): Text.Range =
point_range(text_area.getBuffer, text_area.getCaretPosition)
- def before_caret_range(text_area: TextArea, rendering: Rendering): Text.Range =
+ def before_caret_range(text_area: TextArea, rendering: JEdit_Rendering): Text.Range =
{
val snapshot = rendering.snapshot
val former_caret = snapshot.revert(text_area.getCaretPosition)