--- a/src/Pure/General/symbol_pos.ML Sat Mar 01 19:55:01 2014 +0100
+++ b/src/Pure/General/symbol_pos.ML Sat Mar 01 22:46:31 2014 +0100
@@ -37,6 +37,7 @@
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
@@ -232,6 +233,7 @@
(* compact representation -- with Symbol.DEL padding *)
type text = string;
+type source = {delimited: bool, text: text, pos: Position.T}
fun pad [] = []
| pad [(s, _)] = [s]