src/Tools/jEdit/src/jedit_lib.scala
changeset 64621 7116f2634e32
parent 63426 2e4de628201f
child 64730 76996d915894
--- 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)