# HG changeset patch
# User wenzelm
# Date 1395052786 -3600
# Node ID 31289387fdf80f9bb527941f2baa2a6996f6edb0
# Parent  15351577da10396a839a85f95dad614e4ba5e4b2
tuned signature;

diff -r 15351577da10 -r 31289387fdf8 src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Mon Mar 17 11:33:09 2014 +0100
+++ b/src/Pure/PIDE/text.scala	Mon Mar 17 11:39:46 2014 +0100
@@ -26,6 +26,8 @@
   {
     def apply(start: Offset): Range = Range(start, start)
 
+    val offside: Range = apply(-1)
+
     object Ordering extends scala.math.Ordering[Text.Range]
     {
       def compare(r1: Text.Range, r2: Text.Range): Int = r1 compare r2
diff -r 15351577da10 -r 31289387fdf8 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Mar 17 11:33:09 2014 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Mar 17 11:39:46 2014 +0100
@@ -305,7 +305,7 @@
 
     val caret_range =
       if (caret_enabled) JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
-      else Text.Range(-1)
+      else Text.Range.offside
 
     var w = 0.0f
     var chunk = head