src/Tools/jEdit/src/jedit_lib.scala
changeset 56574 2b38472a4695
parent 56457 eea4bbe15745
child 56587 83777a91f5de
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Apr 14 20:36:50 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Apr 14 21:51:41 2014 +0200
     1.3 @@ -176,6 +176,16 @@
     1.4      }
     1.5  
     1.6  
     1.7 +  /* caret */
     1.8 +
     1.9 +  def before_caret_range(text_area: TextArea, rendering: Rendering): Text.Range =
    1.10 +  {
    1.11 +    val snapshot = rendering.snapshot
    1.12 +    val former_caret = snapshot.revert(text_area.getCaretPosition)
    1.13 +    snapshot.convert(Text.Range(former_caret - 1, former_caret))
    1.14 +  }
    1.15 +
    1.16 +
    1.17    /* text ranges */
    1.18  
    1.19    def buffer_range(buffer: JEditBuffer): Text.Range =