--- a/src/Pure/PIDE/text.scala Tue Aug 12 15:31:24 2014 +0200
+++ b/src/Pure/PIDE/text.scala Tue Aug 12 15:46:20 2014 +0200
@@ -40,7 +40,7 @@
if (start > stop)
error("Bad range: [" + start.toString + ":" + stop.toString + "]")
- override def toString = "[" + start.toString + ":" + stop.toString + "]"
+ override def toString: String = "[" + start.toString + ":" + stop.toString + "]"
def length: Int = stop - start
@@ -116,7 +116,7 @@
case other: Perspective => ranges == other.ranges
case _ => false
}
- override def toString = ranges.toString
+ override def toString: String = ranges.toString
}
@@ -141,7 +141,7 @@
final class Edit private(val is_insert: Boolean, val start: Offset, val text: String)
{
- override def toString =
+ override def toString: String =
(if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"