src/Pure/PIDE/line.scala

--- a/src/Pure/PIDE/line.scala	Sun Nov 02 14:42:46 2025 +0100
+++ b/src/Pure/PIDE/line.scala	Sun Nov 02 15:53:04 2025 +0100
@@ -84,6 +84,10 @@
     def line1: Int = pos.line1
     def column: Int = pos.column
     def column1: Int = pos.column1
+
+    def advance(text: String): Node_Position =
+      if (text.isEmpty) this
+      else copy(pos = pos.advance(text))
   }
 
   sealed case class Node_Range(name: String, range: Range = Range.zero) {