--- a/src/Pure/General/bytes.scala Sat Oct 01 13:08:34 2022 +0000
+++ b/src/Pure/General/bytes.scala Sat Oct 01 21:58:08 2022 +0200
@@ -131,6 +131,11 @@
def text: String = UTF8.decode_permissive(this)
+ def wellformed_text: Option[String] = {
+ val s = text
+ if (this == Bytes(s)) Some(s) else None
+ }
+
def encode_base64: String = {
val b =
if (offset == 0 && length == bytes.length) bytes
@@ -138,10 +143,11 @@
Base64.encode(b)
}
- def maybe_encode_base64: (Boolean, String) = {
- val s = text
- if (this == Bytes(s)) (false, s) else (true, encode_base64)
- }
+ def maybe_encode_base64: (Boolean, String) =
+ wellformed_text match {
+ case Some(s) => (false, s)
+ case None => (true, encode_base64)
+ }
override def toString: String = "Bytes(" + length + ")"
--- a/src/Pure/General/symbol.scala Sat Oct 01 13:08:34 2022 +0000
+++ b/src/Pure/General/symbol.scala Sat Oct 01 21:58:08 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) {
--- a/src/Pure/PIDE/command.scala Sat Oct 01 13:08:34 2022 +0000
+++ b/src/Pure/PIDE/command.scala Sat Oct 01 21:58:08 2022 +0200
@@ -553,7 +553,7 @@
val core_range: Text.Range =
Text.Range(0,
- span.content.reverse.iterator.takeWhile(_.is_ignored).foldLeft(length)(_ - _.source.length))
+ span.content.reverseIterator.takeWhile(_.is_ignored).foldLeft(length)(_ - _.source.length))
def source(range: Text.Range): String = range.substring(source)
--- a/src/Pure/PIDE/document.scala Sat Oct 01 13:08:34 2022 +0000
+++ b/src/Pure/PIDE/document.scala Sat Oct 01 21:58:08 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 =
--- a/src/Pure/PIDE/rendering.scala Sat Oct 01 13:08:34 2022 +0000
+++ b/src/Pure/PIDE/rendering.scala Sat Oct 01 21:58:08 2022 +0200
@@ -398,12 +398,14 @@
/* spell checker */
- private lazy val spell_checker_include =
+ lazy val spell_checker_include: Markup.Elements =
Markup.Elements(space_explode(',', options.string("spell_checker_include")): _*)
- private lazy val spell_checker_elements =
- spell_checker_include ++
- Markup.Elements(space_explode(',', options.string("spell_checker_exclude")): _*)
+ lazy val spell_checker_exclude: Markup.Elements =
+ Markup.Elements(space_explode(',', options.string("spell_checker_exclude")): _*)
+
+ lazy val spell_checker_elements: Markup.Elements =
+ spell_checker_include ++ spell_checker_exclude
def spell_checker(range: Text.Range): List[Text.Info[Text.Range]] = {
val result =
--- a/src/Pure/PIDE/text.scala Sat Oct 01 13:08:34 2022 +0000
+++ b/src/Pure/PIDE/text.scala Sat Oct 01 21:58:08 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