src/Pure/General/symbol_pos.ML
changeset 55828 42ac3cfb89f6
parent 55709 4e5a83a46ded
child 55829 b7bdea5336dd
     1.1 --- a/src/Pure/General/symbol_pos.ML	Sat Mar 01 19:55:01 2014 +0100
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Sat Mar 01 22:46:31 2014 +0100
     1.3 @@ -37,6 +37,7 @@
     1.4    val source: Position.T -> (Symbol.symbol, 'a) Source.source ->
     1.5      (T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source
     1.6    type text = string
     1.7 +  type source = {delimited: bool, text: text, pos: Position.T}
     1.8    val implode: T list -> text
     1.9    val implode_range: Position.T -> Position.T -> T list -> text * Position.range
    1.10    val explode: text * Position.T -> T list
    1.11 @@ -232,6 +233,7 @@
    1.12  (* compact representation -- with Symbol.DEL padding *)
    1.13  
    1.14  type text = string;
    1.15 +type source = {delimited: bool, text: text, pos: Position.T}
    1.16  
    1.17  fun pad [] = []
    1.18    | pad [(s, _)] = [s]