# HG changeset patch # User wenzelm # Date 1664647856 -7200 # Node ID 16c12979c132a67990b357cd4d640b25e72e12d8 # Parent 035ffcd82fb2c5cff2fdee4d17e013042a51cab2 tuned signature; diff -r 035ffcd82fb2 -r 16c12979c132 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Sat Oct 01 16:07:05 2022 +0200 +++ b/src/Pure/General/symbol.scala Sat Oct 01 20:10:56 2022 +0200 @@ -211,7 +211,7 @@ case class File(name: String) extends Name def apply(text: CharSequence): Text_Chunk = - new Text_Chunk(Text.Range(0, text.length), Index(text)) + new Text_Chunk(Text.Range.length(text), Index(text)) } final class Text_Chunk private(val range: Text.Range, private val index: Index) { diff -r 035ffcd82fb2 -r 16c12979c132 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Sat Oct 01 16:07:05 2022 +0200 +++ b/src/Pure/PIDE/document.scala Sat Oct 01 20:10:56 2022 +0200 @@ -611,7 +611,7 @@ val xml = if (Bytes(text) == bytes) { val markup = command.init_markups(Command.Markup_Index.blob(blob)) - markup.to_XML(Text.Range(0, text.length), text, elements) + markup.to_XML(Text.Range.length(text), text, elements) } else Nil blob -> xml @@ -1161,7 +1161,7 @@ } yield tree).toList } else { - Text.Range(0, node.source.length).try_restrict(range) match { + Text.Range.length(node.source).try_restrict(range) match { case None => Nil case Some(node_range) => val markup = diff -r 035ffcd82fb2 -r 16c12979c132 src/Pure/PIDE/text.scala --- a/src/Pure/PIDE/text.scala Sat Oct 01 16:07:05 2022 +0200 +++ b/src/Pure/PIDE/text.scala Sat Oct 01 20:10:56 2022 +0200 @@ -22,7 +22,9 @@ object Range { def apply(start: Offset): Range = Range(start, start) + def length(text: CharSequence): Range = Range(0, text.length) + val zero: Range = apply(0) val full: Range = apply(0, Integer.MAX_VALUE / 2) val offside: Range = apply(-1) @@ -108,7 +110,7 @@ ) { def is_empty: Boolean = ranges.isEmpty def range: Range = - if (is_empty) Range(0) + if (is_empty) Range.zero else Range(ranges.head.start, ranges.last.stop) override def hashCode: Int = ranges.hashCode