# 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 }