tuned signature;
authorwenzelm
Thu Apr 20 11:38:42 2017 +0200 (2017-04-20 ago)
changeset 655224d7c5df70a14
parent 65521 e307a781416a
child 65523 4f2954adc217
tuned signature;
src/Pure/PIDE/command.scala
src/Pure/PIDE/line.scala
src/Pure/PIDE/text.scala
src/Tools/jEdit/src/jedit_lib.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Thu Apr 20 11:33:36 2017 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Thu Apr 20 11:38:42 2017 +0200
     1.3 @@ -520,7 +520,7 @@
     1.4      Text.Range(0,
     1.5        (length /: span.content.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length))
     1.6  
     1.7 -  def source(range: Text.Range): String = source.substring(range.start, range.stop)
     1.8 +  def source(range: Text.Range): String = range.substring(source)
     1.9  
    1.10  
    1.11    /* accumulated results */
     2.1 --- a/src/Pure/PIDE/line.scala	Thu Apr 20 11:33:36 2017 +0200
     2.2 +++ b/src/Pure/PIDE/line.scala	Thu Apr 20 11:38:42 2017 +0200
     2.3 @@ -123,8 +123,7 @@
     2.4      lazy val text: String = Document.text(lines)
     2.5  
     2.6      def try_get_text(range: Text.Range): Option[String] =
     2.7 -      if (text_range.contains(range)) Some(text.substring(range.start, range.stop))
     2.8 -      else None
     2.9 +      if (text_range.contains(range)) Some(range.substring(text)) else None
    2.10  
    2.11      override def toString: String = text
    2.12  
     3.1 --- a/src/Pure/PIDE/text.scala	Thu Apr 20 11:33:36 2017 +0200
     3.2 +++ b/src/Pure/PIDE/text.scala	Thu Apr 20 11:38:42 2017 +0200
     3.3 @@ -71,6 +71,8 @@
     3.4      def try_join(that: Range): Option[Range] =
     3.5        if (this apart that) None
     3.6        else Some(Range(this.start min that.start, this.stop max that.stop))
     3.7 +
     3.8 +    def substring(text: String): String = text.substring(start, stop)
     3.9    }
    3.10  
    3.11  
     4.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Thu Apr 20 11:33:36 2017 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Thu Apr 20 11:38:42 2017 +0200
     4.3 @@ -176,7 +176,7 @@
     4.4      catch { case _: ArrayIndexOutOfBoundsException => None }
     4.5  
     4.6    def try_get_text(text: String, range: Text.Range): Option[String] =
     4.7 -    try { Some(text.substring(range.start, range.stop)) }
     4.8 +    try { Some(range.substring(text)) }
     4.9      catch { case _: IndexOutOfBoundsException => None }
    4.10  
    4.11