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) {