src/Pure/PIDE/command_span.scala

--- a/src/Pure/PIDE/command_span.scala	Fri Dec 18 12:57:25 2020 +0100
+++ b/src/Pure/PIDE/command_span.scala	Fri Dec 18 23:19:07 2020 +0100
@@ -8,6 +8,7 @@
 
 
 import scala.collection.mutable
+import scala.util.parsing.input.CharSequenceReader
 
 
 object Command_Span
@@ -89,6 +90,8 @@
     def is_begin: Boolean = content.exists(_.is_begin)
     def is_end: Boolean = content.exists(_.is_end)
 
+    def content_reader: CharSequenceReader = Scan.char_reader(Token.implode(content))
+
     def length: Int = (0 /: content)(_ + _.source.length)
 
     def compact_source: (String, Span) =