# HG changeset patch
# User wenzelm
# Date 1664654288 -7200
# Node ID 0a44395a25f0bafa7497c1ce0bda7f55417b9536
# Parent  a7ccb744047b320777c0dbfa350319f6eee3fea1# Parent  03dd2f19f1d738d3bbf44668e7df32c568ef9477
merged

diff -r a7ccb744047b -r 0a44395a25f0 src/Pure/General/bytes.scala
--- 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 + ")"
 
diff -r a7ccb744047b -r 0a44395a25f0 src/Pure/General/symbol.scala
--- 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) {
diff -r a7ccb744047b -r 0a44395a25f0 src/Pure/PIDE/command.scala
--- 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)
 
diff -r a7ccb744047b -r 0a44395a25f0 src/Pure/PIDE/document.scala
--- 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 =
diff -r a7ccb744047b -r 0a44395a25f0 src/Pure/PIDE/rendering.scala
--- 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 =
diff -r a7ccb744047b -r 0a44395a25f0 src/Pure/PIDE/text.scala
--- 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