# HG changeset patch
# User wenzelm
# Date 1492681122 -7200
# Node ID 4d7c5df70a1403f8116edf692bde860b154a31cc
# Parent  e307a781416ab86623dd779a64d4f2621eff8c05
tuned signature;

diff -r e307a781416a -r 4d7c5df70a14 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 */
diff -r e307a781416a -r 4d7c5df70a14 src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Thu Apr 20 11:33:36 2017 +0200
+++ b/src/Pure/PIDE/line.scala	Thu Apr 20 11:38:42 2017 +0200
@@ -123,8 +123,7 @@
     lazy val text: String = Document.text(lines)
 
     def try_get_text(range: Text.Range): Option[String] =
-      if (text_range.contains(range)) Some(text.substring(range.start, range.stop))
-      else None
+      if (text_range.contains(range)) Some(range.substring(text)) else None
 
     override def toString: String = text
 
diff -r e307a781416a -r 4d7c5df70a14 src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Thu Apr 20 11:33:36 2017 +0200
+++ b/src/Pure/PIDE/text.scala	Thu Apr 20 11:38:42 2017 +0200
@@ -71,6 +71,8 @@
     def try_join(that: Range): Option[Range] =
       if (this apart that) None
       else Some(Range(this.start min that.start, this.stop max that.stop))
+
+    def substring(text: String): String = text.substring(start, stop)
   }
 
 
diff -r e307a781416a -r 4d7c5df70a14 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Thu Apr 20 11:33:36 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Thu Apr 20 11:38:42 2017 +0200
@@ -176,7 +176,7 @@
     catch { case _: ArrayIndexOutOfBoundsException => None }
 
   def try_get_text(text: String, range: Text.Range): Option[String] =
-    try { Some(text.substring(range.start, range.stop)) }
+    try { Some(range.substring(text)) }
     catch { case _: IndexOutOfBoundsException => None }