src/Pure/General/symbol_pos.ML
changeset 58047 9f3826352b52
parent 55829 b7bdea5336dd
child 58850 1bb0ad7827b4
     1.1 --- a/src/Pure/General/symbol_pos.ML	Wed Aug 27 12:32:07 2014 +0200
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Wed Aug 27 12:32:42 2014 +0200
     1.3 @@ -41,6 +41,7 @@
     1.4    val implode_range: Position.T -> Position.T -> T list -> text * Position.range
     1.5    val explode: text * Position.T -> T list
     1.6    type source = {delimited: bool, text: text, pos: Position.T}
     1.7 +  val source_explode: source -> T list
     1.8    val source_content: source -> string * Position.T
     1.9    val scan_ident: T list -> T list * T list
    1.10    val is_identifier: string -> bool
    1.11 @@ -261,6 +262,8 @@
    1.12  
    1.13  type source = {delimited: bool, text: text, pos: Position.T};
    1.14  
    1.15 +fun source_explode {delimited = _, text, pos} = explode (text, pos);
    1.16 +
    1.17  fun source_content {delimited = _, text, pos} =
    1.18    let val syms = explode (text, pos) in (content syms, pos) end;
    1.19