--- a/src/Pure/General/symbol_pos.ML Wed Aug 27 12:32:07 2014 +0200
+++ b/src/Pure/General/symbol_pos.ML Wed Aug 27 12:32:42 2014 +0200
@@ -41,6 +41,7 @@
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_explode: source -> T list
val source_content: source -> string * Position.T
val scan_ident: T list -> T list * T list
val is_identifier: string -> bool
@@ -261,6 +262,8 @@
type source = {delimited: bool, text: text, pos: Position.T};
+fun source_explode {delimited = _, text, pos} = explode (text, pos);
+
fun source_content {delimited = _, text, pos} =
let val syms = explode (text, pos) in (content syms, pos) end;