# HG changeset patch
# User wenzelm
# Date 1482351464 -3600
# Node ID bbfcef118acbf88e2b6e650cb9dd04c73cebaefc
# Parent  805c5e6fa430da59177a0c01dc0b1b303ec0d27e
clarified border cases;

diff -r 805c5e6fa430 -r bbfcef118acb src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Wed Dec 21 16:32:34 2016 +0100
+++ b/src/Pure/PIDE/line.scala	Wed Dec 21 21:17:44 2016 +0100
@@ -44,12 +44,19 @@
 
   /* range (right-open interval) */
 
+  object Range
+  {
+    val zero: Range = Range(Position.zero, Position.zero)
+  }
+
   sealed case class Range(start: Position, stop: Position)
   {
     if (start.compare(stop) > 0)
       error("Bad line range: " + start.print + ".." + stop.print)
 
-    def print: String = start.print + ".." + stop.print
+    def print: String =
+      if (start == stop) start.print
+      else start.print + ".." + stop.print
   }