--- a/src/Pure/PIDE/text.scala Sat Dec 10 17:20:39 2016 +0100
+++ b/src/Pure/PIDE/text.scala Sat Dec 10 17:22:47 2016 +0100
@@ -37,9 +37,9 @@
{
// denotation: {start} Un {i. start < i & i < stop}
if (start > stop)
- error("Bad range: [" + start.toString + ":" + stop.toString + "]")
+ error("Bad range: [" + start.toString + ".." + stop.toString + "]")
- override def toString: String = "[" + start.toString + ":" + stop.toString + "]"
+ override def toString: String = "[" + start.toString + ".." + stop.toString + "]"
def length: Int = stop - start