src/Pure/General/symbol_pos.ML
changeset 58978 e42da880c61e
parent 58864 505a8150368a
child 59064 a8bcb5a446c8
     1.1 --- a/src/Pure/General/symbol_pos.ML	Tue Nov 11 15:55:31 2014 +0100
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Tue Nov 11 18:16:25 2014 +0100
     1.3 @@ -39,7 +39,7 @@
     1.4    val implode: T list -> text
     1.5    val implode_range: Position.T -> Position.T -> T list -> text * Position.range
     1.6    val explode: text * Position.T -> T list
     1.7 -  type source = {delimited: bool, text: text, pos: Position.T}
     1.8 +  type source = {delimited: bool, text: text, range: Position.range}
     1.9    val source_explode: source -> T list
    1.10    val source_content: source -> string * Position.T
    1.11    val scan_ident: T list -> T list * T list
    1.12 @@ -255,11 +255,11 @@
    1.13  
    1.14  (* full source information *)
    1.15  
    1.16 -type source = {delimited: bool, text: text, pos: Position.T};
    1.17 +type source = {delimited: bool, text: text, range: Position.range};
    1.18  
    1.19 -fun source_explode {delimited = _, text, pos} = explode (text, pos);
    1.20 +fun source_explode {delimited = _, text, range = (pos, _)} = explode (text, pos);
    1.21  
    1.22 -fun source_content {delimited = _, text, pos} =
    1.23 +fun source_content {delimited = _, text, range = (pos, _)} =
    1.24    let val syms = explode (text, pos) in (content syms, pos) end;
    1.25  
    1.26