# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1719754352 -7200
# Node ID fe9ae6b67c29598d67eff9395328277d0637f5db
# Parent  159d1b09fe66d4db75ef55f0238f3755dfc2fe81
clarified PIDE/line range conversions;

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)
diff -r 159d1b09fe66 -r fe9ae6b67c29 src/Tools/VSCode/src/vscode_model.scala
--- a/src/Tools/VSCode/src/vscode_model.scala	Sun Jun 30 15:32:26 2024 +0200
+++ b/src/Tools/VSCode/src/vscode_model.scala	Sun Jun 30 15:32:32 2024 +0200
@@ -29,7 +29,7 @@
   sealed case class Content(node_name: Document.Node.Name, doc: Line.Document) {
     override def toString: String = doc.toString
     def text_length: Text.Offset = doc.text_length
-    def text_range: Text.Range = doc.text_range
+    def text_range: Text.Range = doc.full_range
     def text: String = doc.text
 
     lazy val bytes: Bytes = Bytes(Symbol.encode(text))