src/Pure/PIDE/command.scala

--- a/src/Pure/PIDE/command.scala	Thu Apr 20 11:33:36 2017 +0200
+++ b/src/Pure/PIDE/command.scala	Thu Apr 20 11:38:42 2017 +0200
@@ -520,7 +520,7 @@
     Text.Range(0,
       (length /: span.content.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length))
 
-  def source(range: Text.Range): String = source.substring(range.start, range.stop)
+  def source(range: Text.Range): String = range.substring(source)
 
 
   /* accumulated results */