diff -r 159d1b09fe66 -r fe9ae6b67c29 src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Sun Jun 30 15:32:26 2024 +0200
+++ b/src/Pure/PIDE/line.scala	Sun Jun 30 15:32:32 2024 +0200
@@ -118,12 +118,15 @@
 
   sealed case class Document(lines: List[Line]) {
     lazy val text_length: Text.Offset = Document.length(lines)
-    def text_range: Text.Range = Text.Range(0, text_length)
+    def full_range: Text.Range = Text.Range(0, text_length)
 
     lazy val text: String = Document.text(lines)
 
     def get_text(range: Text.Range): Option[String] =
-      if (text_range.contains(range)) Some(range.substring(text)) else None
+      if (full_range.contains(range)) Some(range.substring(text)) else None
+
+    def get_text(range: Line.Range): Option[String] =
+      text_range(range).flatMap(get_text)
 
     override def toString: String = text
 
@@ -170,6 +173,12 @@
       else None
     }
 
+    def text_range(line_range: Range): Option[Text.Range] =
+      for {
+        start <- offset(line_range.start)
+        stop <- offset(line_range.stop)
+      } yield Text.Range(start, stop)
+
     def change(remove: Range, insert: String): Option[(List[Text.Edit], Document)] = {
       for {
         edit_start <- offset(remove.start)