tuned signature;
authorwenzelm
Mon Mar 17 11:39:46 2014 +0100 (2014-03-17)
changeset 5617231289387fdf8
parent 56171 15351577da10
child 56173 62f10624339a
tuned signature;
src/Pure/PIDE/text.scala
src/Tools/jEdit/src/rich_text_area.scala
     1.1 --- a/src/Pure/PIDE/text.scala	Mon Mar 17 11:33:09 2014 +0100
     1.2 +++ b/src/Pure/PIDE/text.scala	Mon Mar 17 11:39:46 2014 +0100
     1.3 @@ -26,6 +26,8 @@
     1.4    {
     1.5      def apply(start: Offset): Range = Range(start, start)
     1.6  
     1.7 +    val offside: Range = apply(-1)
     1.8 +
     1.9      object Ordering extends scala.math.Ordering[Text.Range]
    1.10      {
    1.11        def compare(r1: Text.Range, r2: Text.Range): Int = r1 compare r2
     2.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Mar 17 11:33:09 2014 +0100
     2.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Mar 17 11:39:46 2014 +0100
     2.3 @@ -305,7 +305,7 @@
     2.4  
     2.5      val caret_range =
     2.6        if (caret_enabled) JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
     2.7 -      else Text.Range(-1)
     2.8 +      else Text.Range.offside
     2.9  
    2.10      var w = 0.0f
    2.11      var chunk = head