src/Pure/General/symbol_pos.ML

   val scan_comment_body: string -> T list -> T list * T list
   val recover_comment: T list -> T list * T list
   val source: Position.T -> (Symbol.symbol, 'a) Source.source ->
     (T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source
   type text = string
-  type source = {delimited: bool, text: text, pos: Position.T}
   val implode: T list -> text
   val implode_range: Position.T -> Position.T -> T list -> text * Position.range
   val explode: text * Position.T -> T list
+  type source = {delimited: bool, text: text, pos: Position.T}
+  val source_content: source -> string * Position.T
   val scan_ident: T list -> T list * T list
   val is_identifier: string -> bool
 end;
 
 structure Symbol_Pos: SYMBOL_POS =

 
 
 (* compact representation -- with Symbol.DEL padding *)
 
 type text = string;
-type source = {delimited: bool, text: text, pos: Position.T}
 
 fun pad [] = []
   | pad [(s, _)] = [s]
   | pad ((s1, pos1) :: (rest as (_, pos2) :: _)) =
       let

       fold (fn s => fn (res, p) => ((s, p) :: res, Position.advance s p))
         (Symbol.explode str) ([], Position.reset_range pos);
   in fold (fn (s, p) => if s = Symbol.DEL then I else cons (s, p)) res [] end;
 
 
+(* full source information *)
+
+type source = {delimited: bool, text: text, pos: Position.T};
+
+fun source_content {delimited = _, text, pos} =
+  let val syms = explode (text, pos) in (content syms, pos) end;
+
+
 (* identifiers *)
 
 local
 
 val letter = Scan.one (symbol #> Symbol.is_letter);